Theorem exnalimn

Description: Existential quantification of a conjunction expressed with only primitive symbols ( -> , -. , A. ). (Contributed by NM, 10-May-1993) State the most general instance. (Revised by BJ, 29-Sep-2019)

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

Proof

Step	Hyp	Ref	Expression
1		alinexa	$$⊢\forall x\left(\phi \to \neg \psi \right)\leftrightarrow \neg \exists x\left(\phi \wedge \psi \right)$$
2	1	con2bii	$$⊢\exists x\left(\phi \wedge \psi \right)\leftrightarrow \neg \forall x\left(\phi \to \neg \psi \right)$$