Theorem eeanv 1944

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

Syntax hints:   /\ wa 104   <-> wb 105   E.wex 1503

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-17 1537  ax-ial 1545

This theorem depends on definitions:  df-bi 117  df-nf 1472

This theorem is referenced by:  eeeanv  1945  ee4anv  1946  2eu4  2131  cgsex2g  2788  cgsex4g  2789  vtocl2  2807  spc2egv  2842  spc2gv  2843  dtruarb  4206  copsex2t  4260  copsex2g  4261  opelopabsb  4275  xpmlem  5064  fununi  5299  imain  5313  brabvv  5937  spc2ed  6252  tfrlem7  6336  ener  6797  domtr  6803  unen  6834  mapen  6864  sbthlemi10  6983  ltexprlemdisj  7623  recexprlemdisj  7647  hashfacen  10834  summodc  11409