- AND_IMP
-
⊢ ∀A B C. A ∧ B ⇒ C ⇔ A ⇒ B ⇒ C
- AND_INV
-
⊢ ∀A. ¬A ∧ A ⇔ F
- AND_INV2
-
⊢ (¬A ⇒ F) ⇒ (A ⇒ F) ⇒ F
- AND_INV_IMP
-
⊢ ∀A. A ⇒ ¬A ⇒ F
- EQF_Imp1
-
⊢ ∀b. ¬b ⇒ (b ⇔ F)
- EQT_Imp1
-
⊢ ∀b. b ⇒ (b ⇔ T)
- NOT_ELIM2
-
⊢ ¬A ⇒ F ⇔ A
- NOT_NOT
-
⊢ ∀t. ¬¬t ⇔ t
- 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
- dc_cond
-
⊢ (p ⇔ if q then r else s) ⇔
(p ∨ q ∨ ¬s) ∧ (p ∨ ¬r ∨ ¬q) ∧ (p ∨ ¬r ∨ ¬s) ∧ (¬q ∨ r ∨ ¬p) ∧ (q ∨ s ∨ ¬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_eq
-
⊢ (p ⇔ (q ⇔ r)) ⇔ (p ∨ q ∨ r) ∧ (p ∨ ¬r ∨ ¬q) ∧ (q ∨ ¬r ∨ ¬p) ∧ (r ∨ ¬q ∨ ¬p)
- dc_imp
-
⊢ (p ⇔ q ⇒ r) ⇔ (p ∨ q) ∧ (p ∨ ¬r) ∧ (¬q ∨ r ∨ ¬p)
- dc_neg
-
⊢ (p ⇔ ¬q) ⇔ (p ∨ q) ∧ (¬q ∨ ¬p)
- pth_an1
-
⊢ p ∧ q ⇒ p
- pth_an2
-
⊢ p ∧ q ⇒ q
- pth_ni1
-
⊢ ¬(p ⇒ q) ⇒ p
- pth_ni2
-
⊢ ¬(p ⇒ q) ⇒ ¬q
- pth_nn
-
⊢ ¬¬p ⇒ p
- pth_no1
-
⊢ ¬(p ∨ q) ⇒ ¬p
- pth_no2
-
⊢ ¬(p ∨ q) ⇒ ¬q