nanbi - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > nanbi		Unicode version

Theorem nanbi 1294

Description: Show equivalence between the bidirectional and the Nicod version. (Contributed by Jeff Hoffman, 19-Nov-2007.)

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

**Proof of Theorem nanbi**
Step	Hyp	Ref	Expression
1		pm4.57 483	. 2 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
2		df-nan 1288	. . 3 $-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $/\$ $-/\$ $-/\$ $-/\$
3		df-nan 1288	. . . 4 $-/\$ $/\$
4		df-nan 1288	. . . . 5 $-/\$ $-/\$ $-/\$ $-/\$ $/\$ $-/\$
5		nannot 1293	. . . . . 6 $-/\$
6		nannot 1293	. . . . . 6 $-/\$
7	5, 6	anbi12i 678	. . . . 5 $/\$ $-/\$ $/\$ $-/\$
8	4, 7	xchbinxr 302	. . . 4 $-/\$ $-/\$ $-/\$ $/\$
9	3, 8	anbi12i 678	. . 3 $-/\$ $/\$ $-/\$ $-/\$ $-/\$ $/\$ $/\$ $/\$
10	2, 9	xchbinx 301	. 2 $-/\$ $-/\$ $-/\$ $-/\$ $-/\$ $/\$ $/\$ $/\$
11		dfbi3 863	. 2 $/\$ $\/$ $/\$
12	1, 10, 11	3bitr4ri 269	1 $-/\$ $-/\$ $-/\$ $-/\$ $-/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 176 $\/$ wo 357 $/\$ wa 358 $-/\$ wnan 1287

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 df-nan 1288

This theorem is referenced by: nic-dfim 1434 nic-dfneg 1435