Theorem alinexa

Description: A transformation of quantifiers and logical connectives. (Contributed by NM, 19-Aug-1993)

	Ref	Expression
Assertion	alinexa	$$⊢\forall x\left(\phi \to \neg \psi \right)\leftrightarrow \neg \exists x\left(\phi \wedge \psi \right)$$

Proof

Step	Hyp	Ref	Expression
1		imnang	$$⊢\forall x\left(\phi \to \neg \psi \right)\leftrightarrow \forall x\neg \left(\phi \wedge \psi \right)$$
2		alnex	$$⊢\forall x\neg \left(\phi \wedge \psi \right)\leftrightarrow \neg \exists x\left(\phi \wedge \psi \right)$$
3	1 2	bitri	$$⊢\forall x\left(\phi \to \neg \psi \right)\leftrightarrow \neg \exists x\left(\phi \wedge \psi \right)$$