Theorem eeanv 1905

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 1509	. 2 |- F/ y ph
2		nfv 1509	. 2 |- F/ x ps
3	1, 2	eean 1904	1 |- ( E. x E. y ( ph /\ ps ) <-> ( E. x ph /\ E. y ps ) )

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

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-ial 1515

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

This theorem is referenced by:  eeeanv  1906  ee4anv  1907  2eu4  2093  cgsex2g  2725  cgsex4g  2726  vtocl2  2744  spc2egv  2779  spc2gv  2780  dtruarb  4123  copsex2t  4175  copsex2g  4176  opelopabsb  4190  xpmlem  4967  fununi  5199  imain  5213  brabvv  5825  spc2ed  6138  tfrlem7  6222  ener  6681  domtr  6687  unen  6718  mapen  6748  sbthlemi10  6862  ltexprlemdisj  7438  recexprlemdisj  7462  hashfacen  10611  summodc  11184