anddi - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > anddi		Unicode version

Theorem anddi 767

Description: Double distributive law for conjunction. (Contributed by NM, 12-Aug-1994.)

**Assertion**
Ref	Expression
anddi	$\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

**Proof of Theorem anddi**
Step	Hyp	Ref	Expression
1		andir 765	. 2 $\/$ $/\$ $\/$ $/\$ $\/$ $\/$ $/\$ $\/$
2		andi 764	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$
3		andi 764	. . 3 $/\$ $\/$ $/\$ $\/$ $/\$
4	2, 3	orbi12i 713	. 2 $/\$ $\/$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$
5	1, 4	bitri 182	1 $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$

Colors of variables: wff set class

Syntax hints: $/\$ wa 102

wb 103 $\/$ wo 661

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 662

This theorem depends on definitions: df-bi 115

This theorem is referenced by: funun 4964 acexmidlemcase 5527 nnm00 6125