Logical implication
Implies is the ACL2 implication function. (implies P Q) means that either P is false (i.e., nil) or Q is true (i.e., not nil).
Function: implies
(defun implies (p q) (declare (xargs :guard t)) (if p (if q t nil) t))
