- AND_IMP
-
|- ∀A B C. A ∧ B ⇒ C ⇔ A ⇒ B ⇒ C
- NOT_NOT
-
|- ∀t. ¬ ¬t ⇔ t
- AND_INV
-
|- ∀A. ¬A ∧ A ⇔ F
- AND_INV_IMP
-
|- ∀A. A ⇒ ¬A ⇒ F
- OR_DUAL
-
|- ¬(A ∨ B) ⇒ F ⇔ ¬A ⇒ ¬B ⇒ F
- OR_DUAL2
-
|- ¬(A ∨ B) ⇒ F ⇔ (A ⇒ F) ⇒ ¬B ⇒ F
- OR_DUAL3
-
|- ¬(¬A ∨ B) ⇒ F ⇔ A ⇒ ¬B ⇒ F
- AND_INV2
-
|- (¬A ⇒ F) ⇒ (A ⇒ F) ⇒ F
- NOT_ELIM2
-
|- ¬A ⇒ F ⇔ A
- EQT_Imp1
-
|- ∀b. b ⇒ (b ⇔ T)
- EQF_Imp1
-
|- ∀b. ¬b ⇒ (b ⇔ F)
- dc_eq
-
|- (p ⇔ (q ⇔ r)) ⇔ (p ∨ q ∨ r) ∧ (p ∨ ¬r ∨ ¬q) ∧ (q ∨ ¬r ∨ ¬p) ∧ (r ∨ ¬q ∨ ¬p)
- dc_conj
-
|- (p ⇔ q ∧ r) ⇔ (p ∨ ¬q ∨ ¬r) ∧ (q ∨ ¬p) ∧ (r ∨ ¬p)
- dc_disj
-
|- (p ⇔ q ∨ r) ⇔ (p ∨ ¬q) ∧ (p ∨ ¬r) ∧ (q ∨ r ∨ ¬p)
- dc_imp
-
|- (p ⇔ q ⇒ r) ⇔ (p ∨ q) ∧ (p ∨ ¬r) ∧ (¬q ∨ r ∨ ¬p)
- dc_neg
-
|- (p ⇔ ¬q) ⇔ (p ∨ q) ∧ (¬q ∨ ¬p)
- dc_cond
-
|- (p ⇔ if q then r else s) ⇔
(p ∨ q ∨ ¬s) ∧ (p ∨ ¬r ∨ ¬q) ∧ (p ∨ ¬r ∨ ¬s) ∧ (¬q ∨ r ∨ ¬p) ∧ (q ∨ s ∨ ¬p)
- pth_ni1
-
|- ¬(p ⇒ q) ⇒ p
- pth_ni2
-
|- ¬(p ⇒ q) ⇒ ¬q
- pth_no1
-
|- ¬(p ∨ q) ⇒ ¬p
- pth_no2
-
|- ¬(p ∨ q) ⇒ ¬q
- pth_an1
-
|- p ∧ q ⇒ p
- pth_an2
-
|- p ∧ q ⇒ q
- pth_nn
-
|- ¬ ¬p ⇒ p