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
|- ( -. ( -. ( -. ( 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 biorfi
 |-  ( 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 )