Theorem 3oran

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

	Ref	Expression
Assertion	3oran	$$⊢\left(\phi \vee \psi \vee \chi \right)\leftrightarrow \neg \left(\neg \phi \wedge \neg \psi \wedge \neg \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		3ioran	$$⊢\neg \left(\phi \vee \psi \vee \chi \right)\leftrightarrow \left(\neg \phi \wedge \neg \psi \wedge \neg \chi \right)$$
2	1	con1bii	$$⊢\neg \left(\neg \phi \wedge \neg \psi \wedge \neg \chi \right)\leftrightarrow \left(\phi \vee \psi \vee \chi \right)$$
3	2	bicomi	$$⊢\left(\phi \vee \psi \vee \chi \right)\leftrightarrow \neg \left(\neg \phi \wedge \neg \psi \wedge \neg \chi \right)$$