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 biorfi ⊢χ↔χ∨¬φ∨ψ∧φ
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 ⊢¬¬¬φ∨ψ∨χ∨¬φ∨¬¬χ∨¬χ∨θ↔χ