IFTHEN : TACTICALIFTHEN is a tactical.
(IFTHEN test tactic1 [tactic2]) will first evaluate test, which may
be either a tactical or (if user is an expert) an arbitrary LISP expression.
If test is a tactical and does not fail, or is a LISP expression which does
not evaluate to nil, then tactic1 will be executed and IFTHEN will return its
results. If test fails or is nil, then tactic2 (if present) will be executed
and its results returned by IFTHEN. Tactic2 is optional; if not specified,
and test fails, IFTHEN will return failure.
TPS documentation homepage