df3nandALT1 - Mathbox for Anthony Hart

	Mathbox for Anthony Hart		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > df3nandALT1		Structured version Visualization version Unicode version

Theorem df3nandALT1 32396

Description: The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011.)

**Assertion**
Ref	Expression
df3nandALT1	$-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $-/\$

**Proof of Theorem df3nandALT1**
Step	Hyp	Ref	Expression
1		iman 440	. . 3 $-/\$ $/\$ $-/\$ $/\$ $-/\$ $/\$ $-/\$
2		imnan 438	. . . . . . . 8 $/\$
3	2	biimpi 206	. . . . . . 7 $/\$
4	3, 3	jca 554	. . . . . 6 $/\$ $/\$ $/\$
5	2	biimpri 218	. . . . . . 7 $/\$
6	5	adantl 482	. . . . . 6 $/\$ $/\$ $/\$
7	4, 6	impbii 199	. . . . 5 $/\$ $/\$ $/\$
8		df-nan 1448	. . . . . 6 $-/\$ $/\$
9	8, 8	anbi12i 733	. . . . 5 $-/\$ $/\$ $-/\$ $/\$ $/\$ $/\$
10	7, 9	bitr4i 267	. . . 4 $-/\$ $/\$ $-/\$
11	10	imbi2i 326	. . 3 $-/\$ $/\$ $-/\$
12		df-nan 1448	. . . . 5 $-/\$ $-/\$ $-/\$ $-/\$ $/\$ $-/\$
13	12	anbi2i 730	. . . 4 $/\$ $-/\$ $-/\$ $-/\$ $/\$ $-/\$ $/\$ $-/\$
14	13	notbii 310	. . 3 $/\$ $-/\$ $-/\$ $-/\$ $/\$ $-/\$ $/\$ $-/\$
15	1, 11, 14	3bitr4i 292	. 2 $/\$ $-/\$ $-/\$ $-/\$
16		df-3nand 32395	. 2 $-/\$ $-/\$
17		df-nan 1448	. 2 $-/\$ $-/\$ $-/\$ $-/\$ $/\$ $-/\$ $-/\$ $-/\$
18	15, 16, 17	3bitr4i 292	1 $-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $-/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $-/\$ wnan 1447 $-/\$ w3nand 32394

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-an 386 df-nan 1448 df-3nand 32395

This theorem is referenced by: (None)