Metamath Proof Explorer

Theorem dn1

Description: A single axiom for Boolean algebra known as DN_1. See McCune, Veroff, Fitelson, Harris, Feist, Wos,Short single axioms for Boolean algebra, Journal of Automated Reasoning, 29(1):1--16, 2002. ( https://www.cs.unm.edu/~mccune/papers/basax/v12.pdf ). (Contributed by Jeff Hankins, 3-Jul-2009) (Proof shortened by Andrew Salmon, 13-May-2011) (Proof shortened by Wolf Lammen, 6-Jan-2013)

Ref Expression
Assertion dn1 ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ χ ∨ ¬ φ ∨ ¬ ¬ χ ∨ ¬ χ ∨ θ ↔ χ

Proof

Step Hyp Ref Expression
1 pm2.45 ⊢ ¬ φ ∨ ψ → ¬ φ
2 imnan ⊢ ¬ φ ∨ ψ → ¬ φ ↔ ¬ ¬ φ ∨ ψ ∧ φ
3 1 2 mpbi ⊢ ¬ ¬ φ ∨ ψ ∧ φ
4 3 biorfri ⊢ χ ↔ χ ∨ ¬ φ ∨ ψ ∧ φ
5 orcom ⊢ χ ∨ ¬ φ ∨ ψ ∧ φ ↔ ¬ φ ∨ ψ ∧ φ ∨ χ
6 ordir ⊢ ¬ φ ∨ ψ ∧ φ ∨ χ ↔ ¬ φ ∨ ψ ∨ χ ∧ φ ∨ χ
7 4 5 6 3bitri ⊢ χ ↔ ¬ φ ∨ ψ ∨ χ ∧ φ ∨ χ
8 pm4.45 ⊢ χ ↔ χ ∧ χ ∨ θ
9 anor ⊢ χ ∧ χ ∨ θ ↔ ¬ ¬ χ ∨ ¬ χ ∨ θ
10 8 9 bitri ⊢ χ ↔ ¬ ¬ χ ∨ ¬ χ ∨ θ
11 10 orbi2i ⊢ φ ∨ χ ↔ φ ∨ ¬ ¬ χ ∨ ¬ χ ∨ θ
12 11 anbi2i ⊢ ¬ φ ∨ ψ ∨ χ ∧ φ ∨ χ ↔ ¬ φ ∨ ψ ∨ χ ∧ φ ∨ ¬ ¬ χ ∨ ¬ χ ∨ θ
13 anor ⊢ ¬ φ ∨ ψ ∨ χ ∧ φ ∨ ¬ ¬ χ ∨ ¬ χ ∨ θ ↔ ¬ ¬ ¬ φ ∨ ψ ∨ χ ∨ ¬ φ ∨ ¬ ¬ χ ∨ ¬ χ ∨ θ
14 7 12 13 3bitrri ⊢ ¬ ¬ ¬ φ ∨ ψ ∨ χ ∨ ¬ φ ∨ ¬ ¬ χ ∨ ¬ χ ∨ θ ↔ χ