Theorem ioran

Description: Negated disjunction in terms of conjunction (De Morgan's law). Compare Theorem *4.56 of WhiteheadRussell p. 120. (Contributed by NM, 3-Jan-1993) (Proof shortened by Andrew Salmon, 7-May-2011)

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

Proof

Step	Hyp	Ref	Expression
1		pm4.65	$$⊢\neg \left(\neg \phi \to \psi \right)\leftrightarrow \left(\neg \phi \wedge \neg \psi \right)$$
2		pm4.64	$$⊢\left(\neg \phi \to \psi \right)\leftrightarrow \left(\phi \vee \psi \right)$$
3	1 2	xchnxbi	$$⊢\neg \left(\phi \vee \psi \right)\leftrightarrow \left(\neg \phi \wedge \neg \psi \right)$$