3oran - New Foundations Explorer

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

Theorem 3oran 951

Description: Triple disjunction in terms of triple conjunction. (Contributed by NM, 8-Oct-2012.)

**Assertion**
Ref	Expression
3oran	$\/$ $\/$ $/\$ $/\$

**Proof of Theorem 3oran**
Step	Hyp	Ref	Expression
1		3ioran 950	. . 3 $\/$ $\/$ $/\$ $/\$
2	1	con1bii 321	. 2 $/\$ $/\$ $\/$ $\/$
3	2	bicomi 193	1 $\/$ $\/$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 176 $\/$ w3o 933 $/\$ w3a 934

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-3or 935 df-3an 936

This theorem is referenced by: (None)