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