Theorem eeanv 1913

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

Assertion

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

Distinct variable groups:   ph,y   ps,x

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

Proof of Theorem eeanv

Step	Hyp	Ref	Expression
1		nfv 1619	. 2 |- F/yph
2		nfv 1619	. 2 |- F/xps
3	1, 2	eean 1912	1 |- (E.xE.y(ph /\ ps) <-> (E.xph /\ E.yps))

Syntax hints:   <-> wb 176   /\ wa 358  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545

This theorem is referenced by:  eeeanv  1914  ee4anv  1915  pm11.07  2115  2eu4  2287  cgsex2g  2892  cgsex4g  2893  vtocl2  2911  spc2egv  2942  opkelcokg  4262  sikexlem  4296  ncfinlower  4484  sfin112  4530  sfinltfin  4536  copsex2t  4609  copsex2g  4610  opeqexb  4621  opelxp  4812  xpnz  5046  dfxp2  5114  fununi  5161  1stfo  5506  2ndfo  5507  brtxp  5784  dmtxp  5803  dmpprod  5841  pw1fnf1o  5856  entr  6039  fundmen  6044  unen  6049  xpen  6056  muccl  6133  muccom  6135  ncaddccl  6145  ncdisjeq  6149  tcdi  6165  ce0addcnnul  6180  ce0nnulb  6183  ceclb  6184  sbthlem3  6206  dflec3  6222  nclenc  6223  lenc  6224  tc11  6229  ce2le  6234  muc0or  6253  fnfrec  6321