3ioran - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > 3ioran		Structured version Visualization version Unicode version

Theorem 3ioran 1056

Description: Negated triple disjunction as triple conjunction. (Contributed by Scott Fenton, 19-Apr-2011.)

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

**Proof of Theorem 3ioran**
Step	Hyp	Ref	Expression
1		ioran 511	. . 3 $\/$ $/\$
2	1	anbi1i 731	. 2 $\/$ $/\$ $/\$ $/\$
3		ioran 511	. . 3 $\/$ $\/$ $\/$ $/\$
4		df-3or 1038	. . 3 $\/$ $\/$ $\/$ $\/$
5	3, 4	xchnxbir 323	. 2 $\/$ $\/$ $\/$ $/\$
6		df-3an 1039	. 2 $/\$ $/\$ $/\$ $/\$
7	2, 5, 6	3bitr4i 292	1 $\/$ $\/$ $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wb 196 $\/$ wo 383 $/\$ wa 384 $\/$ w3o 1036 $/\$ w3a 1037

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 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039

This theorem is referenced by: 3oran 1057 cadnot 1554 lcmftp 15349 prm23ge5 15520 cnfldfunALT 19759 fbunfip 21673 frgrregord013 27253 wl-nfeqfb 33323