dn1 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem dn1 855

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.) (The proof was shortened by Andrew Salmon, 13-May-2011.)

**Assertion**
Ref	Expression
dn1	$\/$ $\/$ $\/$ $\/$ $\/$ $\/$

**Proof of Theorem dn1**
Step	Hyp	Ref	Expression
1		anor 328	. 2 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
2		pm2.45 299	. . . . . . 7 $\/$
3	2	pm2.21d 94	. . . . . 6 $\/$
4		anor 328	. . . . . . . 8 $/\$ $\/$ $\/$ $\/$
5		simpl 346	. . . . . . . 8 $/\$ $\/$
6	4, 5	sylbir 218	. . . . . . 7 $\/$ $\/$
7	6	a1i 8	. . . . . 6 $\/$ $\/$ $\/$
8	3, 7	jaod 469	. . . . 5 $\/$ $\/$ $\/$ $\/$
9		ax-1 4	. . . . 5 $\/$ $\/$ $\/$
10	8, 9	jaoi 368	. . . 4 $\/$ $\/$ $\/$ $\/$ $\/$
11	10	imp 377	. . 3 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
12		olc 290	. . . 4 $\/$ $\/$
13		orc 291	. . . . . . 7 $\/$
14	13	ancli 320	. . . . . 6 $/\$ $\/$
15	14, 4	sylib 215	. . . . 5 $\/$ $\/$
16	15	olcd 295	. . . 4 $\/$ $\/$ $\/$
17	12, 16	jca 310	. . 3 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
18	11, 17	impbii 174	. 2 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
19	1, 18	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