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