dn1OLD - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem dn1OLD 856

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

**Assertion**
Ref	Expression
dn1OLD	$\/$ $\/$ $\/$ $\/$ $\/$ $\/$

**Proof of Theorem dn1OLD**
Step	Hyp	Ref	Expression
1		anor 328	. 2 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
2		ioran 331	. . . . . 6 $\/$ $/\$
3		pm2.24 95	. . . . . . . . . 10
4	3	com23 36	. . . . . . . . 9
5		anor 328	. . . . . . . . . 10 $/\$ $\/$ $\/$ $\/$
6		ax-1 4	. . . . . . . . . . . 12
7	6	a1d 15	. . . . . . . . . . 11
8	7	adantr 425	. . . . . . . . . 10 $/\$ $\/$
9	5, 8	sylbir 218	. . . . . . . . 9 $\/$ $\/$
10	4, 9	jaoi 368	. . . . . . . 8 $\/$ $\/$ $\/$
11	10	com13 37	. . . . . . 7 $\/$ $\/$ $\/$
12	11	imp 377	. . . . . 6 $/\$ $\/$ $\/$ $\/$
13	2, 12	sylbi 216	. . . . 5 $\/$ $\/$ $\/$ $\/$
14		ax-1 4	. . . . 5 $\/$ $\/$ $\/$
15	13, 14	jaoi 368	. . . 4 $\/$ $\/$ $\/$ $\/$ $\/$
16	15	imp 377	. . 3 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
17		olc 290	. . . 4 $\/$ $\/$
18		pm2.24 95	. . . . . . 7
19		pm2.24 95	. . . . . . . . 9
20	19	imp3a 388	. . . . . . . 8 $/\$
21		ioran 331	. . . . . . . 8 $\/$ $/\$
22	20, 21	syl5ib 223	. . . . . . 7 $\/$
23	18, 22	jaod 469	. . . . . 6 $\/$ $\/$
24	23	con3d 111	. . . . 5 $\/$ $\/$
25	24	orrd 250	. . . 4 $\/$ $\/$ $\/$
26	17, 25	jca 310	. . 3 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
27	16, 26	impbii 174	. 2 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
28	1, 27	bitr3i 192	1 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

Colors of variables: wff set class

Syntax hints:

wn 2

wi 3

wb 163 $\/$ wo 239 $/\$ wa 240

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

This theorem depends on definitions: df-bi 164 df-or 241 df-an 242