Theorem dn1 932

Description: A single axiom for Boolean algebra known as DN₁. See http://www-unix.mcs.anl.gov/~mccune/papers/basax/v12.pdf. (Contributed by Jeffrey Hankins, 3-Jul-2009.) (Proof shortened by Andrew Salmon, 13-May-2011.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)

Assertion

Ref	Expression
dn1	|- (-. (-. (-. (ph \/ ps) \/ ch) \/ -. (ph \/ -. (-. ch \/ -. (ch \/ th)))) <-> ch)

Proof of Theorem dn1

Step	Hyp	Ref	Expression
1		pm2.45 386	. . . . 5 |- (-. (ph \/ ps) -> -. ph)
2		imnan 411	. . . . 5 |- ((-. (ph \/ ps) -> -. ph) <-> -. (-. (ph \/ ps) /\ ph))
3	1, 2	mpbi 199	. . . 4 |- -. (-. (ph \/ ps) /\ ph)
4	3	biorfi 396	. . 3 |- (ch <-> (ch \/ (-. (ph \/ ps) /\ ph)))
5		orcom 376	. . . 4 |- ((ch \/ (-. (ph \/ ps) /\ ph)) <-> ((-. (ph \/ ps) /\ ph) \/ ch))
6		ordir 835	. . . 4 |- (((-. (ph \/ ps) /\ ph) \/ ch) <-> ((-. (ph \/ ps) \/ ch) /\ (ph \/ ch)))
7	5, 6	bitri 240	. . 3 |- ((ch \/ (-. (ph \/ ps) /\ ph)) <-> ((-. (ph \/ ps) \/ ch) /\ (ph \/ ch)))
8	4, 7	bitri 240	. 2 |- (ch <-> ((-. (ph \/ ps) \/ ch) /\ (ph \/ ch)))
9		pm4.45 669	. . . . 5 |- (ch <-> (ch /\ (ch \/ th)))
10		anor 475	. . . . 5 |- ((ch /\ (ch \/ th)) <-> -. (-. ch \/ -. (ch \/ th)))
11	9, 10	bitri 240	. . . 4 |- (ch <-> -. (-. ch \/ -. (ch \/ th)))
12	11	orbi2i 505	. . 3 |- ((ph \/ ch) <-> (ph \/ -. (-. ch \/ -. (ch \/ th))))
13	12	anbi2i 675	. 2 |- (((-. (ph \/ ps) \/ ch) /\ (ph \/ ch)) <-> ((-. (ph \/ ps) \/ ch) /\ (ph \/ -. (-. ch \/ -. (ch \/ th)))))
14		anor 475	. 2 |- (((-. (ph \/ ps) \/ ch) /\ (ph \/ -. (-. ch \/ -. (ch \/ th)))) <-> -. (-. (-. (ph \/ ps) \/ ch) \/ -. (ph \/ -. (-. ch \/ -. (ch \/ th)))))
15	8, 13, 14	3bitrri 263	1 |- (-. (-. (-. (ph \/ ps) \/ ch) \/ -. (ph \/ -. (-. ch \/ -. (ch \/ th)))) <-> ch)

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360

This theorem is referenced by: (None)