Theorem exancom 1787

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 466	. 2 |- ( ( ph /\ ps ) <-> ( ps /\ ph ) )
2	1	exbii 1774	1 |- ( E. x ( ph /\ ps ) <-> E. x ( ps /\ ph ) )

Syntax hints:   <-> wb 196   /\ wa 384   E.wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  19.42v  1918  19.42  2105  eupickb  2538  risset  3062  morex  3390  pwpw0  4344  pwsnALT  4429  dfuni2  4438  eluni2  4440  unipr  4449  dfiun2g  4552  cnvco  5308  imadif  5973  uniuni  6971  pceu  15551  gsumval3eu  18305  isch3  28098  tgoldbachgt  30741  bnj1109  30857  bnj1304  30890  bnj849  30995  funpartlem  32049  bj-elsngl  32956  bj-ccinftydisj  33100  motr  34127  eluni2f  39286  ssfiunibd  39523  setrec1lem3  42436