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	|- ( -. ( -. ( -. ( ph \/ ps ) \/ ch ) \/ -. ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) <-> ch )

Proof

Step	Hyp	Ref	Expression
1		pm2.45	|- ( -. ( ph \/ ps ) -> -. ph )
2		imnan	|- ( ( -. ( ph \/ ps ) -> -. ph ) <-> -. ( -. ( ph \/ ps ) /\ ph ) )
3	1 2	mpbi	|- -. ( -. ( ph \/ ps ) /\ ph )
4	3	biorfri	|- ( ch <-> ( ch \/ ( -. ( ph \/ ps ) /\ ph ) ) )
5		orcom	|- ( ( ch \/ ( -. ( ph \/ ps ) /\ ph ) ) <-> ( ( -. ( ph \/ ps ) /\ ph ) \/ ch ) )
6		ordir	|- ( ( ( -. ( ph \/ ps ) /\ ph ) \/ ch ) <-> ( ( -. ( ph \/ ps ) \/ ch ) /\ ( ph \/ ch ) ) )
7	4 5 6	3bitri	|- ( ch <-> ( ( -. ( ph \/ ps ) \/ ch ) /\ ( ph \/ ch ) ) )
8		pm4.45	|- ( ch <-> ( ch /\ ( ch \/ th ) ) )
9		anor	|- ( ( ch /\ ( ch \/ th ) ) <-> -. ( -. ch \/ -. ( ch \/ th ) ) )
10	8 9	bitri	|- ( ch <-> -. ( -. ch \/ -. ( ch \/ th ) ) )
11	10	orbi2i	|- ( ( ph \/ ch ) <-> ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) )
12	11	anbi2i	|- ( ( ( -. ( ph \/ ps ) \/ ch ) /\ ( ph \/ ch ) ) <-> ( ( -. ( ph \/ ps ) \/ ch ) /\ ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) )
13		anor	|- ( ( ( -. ( ph \/ ps ) \/ ch ) /\ ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) <-> -. ( -. ( -. ( ph \/ ps ) \/ ch ) \/ -. ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) )
14	7 12 13	3bitrri	|- ( -. ( -. ( -. ( ph \/ ps ) \/ ch ) \/ -. ( ph \/ -. ( -. ch \/ -. ( ch \/ th ) ) ) ) <-> ch )