Built-in axioms and theorems about logical connectives.
Theorem:
(defthm iff-is-an-equivalence (and (booleanp (iff x y)) (iff x x) (implies (iff x y) (iff y x)) (implies (and (iff x y) (iff y z)) (iff x z))) :rule-classes (:equivalence))
Theorem:
(defthm iff-implies-equal-implies-1 (implies (iff x x-equiv) (equal (implies x y) (implies x-equiv y))) :rule-classes (:congruence))
Theorem:
(defthm iff-implies-equal-implies-2 (implies (iff y y-equiv) (equal (implies x y) (implies x y-equiv))) :rule-classes (:congruence))
Theorem:
(defthm iff-implies-equal-not (implies (iff x x-equiv) (equal (not x) (not x-equiv))) :rule-classes (:congruence))