Theorem anor

Description: Conjunction in terms of disjunction (De Morgan's law). Theorem *4.5 of WhiteheadRussell p. 120. (Contributed by NM, 3-Jan-1993) (Proof shortened by Wolf Lammen, 3-Nov-2012)

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

Proof

Step	Hyp	Ref	Expression
1		notnotb	$$⊢\left(\phi \wedge \psi \right)\leftrightarrow \neg \neg \left(\phi \wedge \psi \right)$$
2		ianor	$$⊢\neg \left(\phi \wedge \psi \right)\leftrightarrow \left(\neg \phi \vee \neg \psi \right)$$
3	1 2	xchbinx	$$⊢\left(\phi \wedge \psi \right)\leftrightarrow \neg \left(\neg \phi \vee \neg \psi \right)$$