orddi - Intuitionistic Logic Explorer

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

Theorem orddi 815

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

**Assertion**
Ref	Expression
orddi	$/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$

**Proof of Theorem orddi**
Step	Hyp	Ref	Expression
1		ordir 812	. 2 $/\$ $\/$ $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
2		ordi 811	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$
3		ordi 811	. . 3 $\/$ $/\$ $\/$ $/\$ $\/$
4	2, 3	anbi12i 457	. 2 $\/$ $/\$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$
5	1, 4	bitri 183	1 $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$ $/\$ $\/$

Colors of variables: wff set class

Syntax hints: $/\$ wa 103

wb 104 $\/$ wo 703

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

This theorem depends on definitions: df-bi 116

This theorem is referenced by: prneimg 3761