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 ¬ ¬ ¬ φ ψ χ ¬ φ ¬ ¬ χ ¬ χ θ χ