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