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	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ¬ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		alinexa	⊢ ( ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) ↔ ¬ ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) )
2	1	con2bii	⊢ ( ∃ 𝑥 ( 𝜑 ∧ 𝜓 ) ↔ ¬ ∀ 𝑥 ( 𝜑 → ¬ 𝜓 ) )