Metamath Proof Explorer


Theorem exancom

Description: Commutation of conjunction inside an existential quantifier. (Contributed by NM, 18-Aug-1993)

Ref Expression
Assertion exancom x φ ψ x ψ φ

Proof

Step Hyp Ref Expression
1 ancom φ ψ ψ φ
2 1 exbii x φ ψ x ψ φ