Theorem exnalimn

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.)

Conclusion

\( \vdash \exists x \, (\varphi \wedge \psi) \leftrightarrow \neg \forall x \, (\varphi \rightarrow \neg \psi) \)

Proof

alinexa

con2bii _