Theorem eeanv 1960

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

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

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

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

This theorem is referenced by:  eeeanv  1961  ee4anv  1962  2eu4  2147  cgsex2g  2808  cgsex4g  2809  vtocl2  2828  spc2egv  2863  spc2gv  2864  dtruarb  4236  copsex2t  4290  copsex2g  4291  opelopabsb  4307  xpmlem  5104  fununi  5343  imain  5357  brabvv  5993  spc2ed  6321  tfrlem7  6405  ener  6873  domtr  6879  unen  6910  mapen  6945  sbthlemi10  7070  ltexprlemdisj  7721  recexprlemdisj  7745  hashfacen  10983  summodc  11727