Theorem eeanv 1961

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

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

This theorem is referenced by:  eeeanv  1962  ee4anv  1963  2eu4  2149  cgsex2g  2813  cgsex4g  2814  vtocl2  2833  spc2egv  2870  spc2gv  2871  dtruarb  4251  copsex2t  4307  copsex2g  4308  opelopabsb  4324  xpmlem  5122  fununi  5361  imain  5375  brabvv  6014  spc2ed  6342  tfrlem7  6426  ener  6894  domtr  6900  unen  6932  mapen  6968  sbthlemi10  7094  ltexprlemdisj  7754  recexprlemdisj  7778  hashfacen  11018  summodc  11809