Theorem eeanv 1904

Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)

Assertion

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

Distinct variable groups:   ph, y   ps, x

Allowed substitution hints:   ph( x)   ps( y)

Proof of Theorem eeanv

Step	Hyp	Ref	Expression
1		nfv 1508	. 2 |- F/ y ph
2		nfv 1508	. 2 |- F/ x ps
3	1, 2	eean 1903	1 |- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )

Syntax hints:   /\ wa 103   <-> wb 104   E.wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437

This theorem is referenced by:  eeeanv  1905  ee4anv  1906  2eu4  2092  cgsex2g  2722  cgsex4g  2723  vtocl2  2741  spc2egv  2775  spc2gv  2776  dtruarb  4115  copsex2t  4167  copsex2g  4168  opelopabsb  4182  xpmlem  4959  fununi  5191  imain  5205  brabvv  5817  spc2ed  6130  tfrlem7  6214  ener  6673  domtr  6679  unen  6710  mapen  6740  sbthlemi10  6854  ltexprlemdisj  7414  recexprlemdisj  7438  hashfacen  10579  summodc  11152