This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( ¬ ( ¬ ( ¬ ( 𝜑 ∨ 𝜓 ) ∨ 𝜒 ) ∨ ¬ ( 𝜑 ∨ ¬ ( ¬ 𝜒 ∨ ¬ ( 𝜒 ∨ 𝜃 ) ) ) ) ↔ 𝜒 )