Theorem exancom 1661

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

Assertion

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

Proof of Theorem exancom

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

This proof depends on syntax axioms:   /\ wa 104   <-> wb 105   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  19.29r  1674  19.42h  1739  19.42  1740  risset  2578  morex  3010  dfuni2  3937  eluni2  3939  unipr  3949  dfiun2g  4044  uniuni  4597  cnvco  4965  imadif  5461  funimaexglem  5464  pceu  13074  bdcuni  16902  bj-axun2  16941