Theorem
exancom
Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993.)
Conclusion
\( \vdash \exists x \, (\varphi \wedge \psi) \leftrightarrow \exists x \, (\psi \wedge \varphi) \)
Proof
ancom
exbii
_
This is the content in the right pane.