Metamath Proof Explorer

Theorem exancom

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

Ref Expression
Assertion exancom 
|- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )

Proof

Step Hyp Ref Expression
1 ancom 
 |-  ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2 1 exbii 
 |-  ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )