andi - New Foundations Explorer

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

Theorem andi 837

Description: Distributive law for conjunction. Theorem *4.4 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 5-Jan-2013.)

**Assertion**
Ref	Expression
andi	$/\$ $\/$ $/\$ $\/$ $/\$

**Proof of Theorem andi**
Step	Hyp	Ref	Expression
1		orc 374	. . 3 $/\$ $/\$ $\/$ $/\$
2		olc 373	. . 3 $/\$ $/\$ $\/$ $/\$
3	1, 2	jaodan 760	. 2 $/\$ $\/$ $/\$ $\/$ $/\$
4		orc 374	. . . 4 $\/$
5	4	anim2i 552	. . 3 $/\$ $/\$ $\/$
6		olc 373	. . . 4 $\/$
7	6	anim2i 552	. . 3 $/\$ $/\$ $\/$
8	5, 7	jaoi 368	. 2 $/\$ $\/$ $/\$ $/\$ $\/$
9	3, 8	impbii 180	1 $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wb 176 $\/$ wo 357 $/\$ wa 358

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

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360

This theorem is referenced by: andir 838 anddi 840 indi 3501 indifdir 3511 unrab 3526 unipr 3905 uniun 3910 unopab 4638 xpundi 4832 coundir 5083 imadif 5171 unpreima 5408 nmembers1lem3 6270

W3C validator