dn1 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > dn1		Structured version Visualization version Unicode version

Theorem dn1 1008

Description: A single axiom for Boolean algebra known as DN₁. 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.)

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

**Proof of Theorem dn1**
Step	Hyp	Ref	Expression
1		pm2.45 412	. . . . 5 $\/$
2		imnan 438	. . . . 5 $\/$ $\/$ $/\$
3	1, 2	mpbi 220	. . . 4 $\/$ $/\$
4	3	biorfi 422	. . 3 $\/$ $\/$ $/\$
5		orcom 402	. . . 4 $\/$ $\/$ $/\$ $\/$ $/\$ $\/$
6		ordir 909	. . . 4 $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$
7	5, 6	bitri 264	. . 3 $\/$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
8	4, 7	bitri 264	. 2 $\/$ $\/$ $/\$ $\/$
9		pm4.45 724	. . . . 5 $/\$ $\/$
10		anor 510	. . . . 5 $/\$ $\/$ $\/$ $\/$
11	9, 10	bitri 264	. . . 4 $\/$ $\/$
12	11	orbi2i 541	. . 3 $\/$ $\/$ $\/$ $\/$
13	12	anbi2i 730	. 2 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $/\$ $\/$ $\/$ $\/$
14		anor 510	. 2 $\/$ $\/$ $/\$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$ $\/$
15	8, 13, 14	3bitrri 287	1 $\/$ $\/$ $\/$ $\/$ $\/$ $\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

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 197 df-or 385 df-an 386

This theorem is referenced by: (None)

W3C validator