Theorem eeanv 2182

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

Assertion

Ref	Expression
eeanv	⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))

Distinct variable groups:   𝜑,𝑦   𝜓,𝑥

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem eeanv

Step	Hyp	Ref	Expression
1		nfv 1843	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1843	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	eean 2181	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 384  ∃wex 1704

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  eeeanv  2183  ee4anv  2184  2mo2  2550  cgsex2g  3239  cgsex4g  3240  vtocl2  3261  spc2egv  3295  dtru  4857  copsex2t  4957  copsex2g  4958  xpnz  5553  fununi  5964  wfrlem4  7418  wfrfun  7425  tfrlem7  7479  ener  8002  enerOLD  8003  domtr  8009  unen  8040  undom  8048  sbthlem10  8079  mapen  8124  infxpenc2  8845  fseqen  8850  dfac5lem4  8949  zorn2lem6  9323  fpwwe2lem12  9463  genpnnp  9827  hashfacen  13238  summo  14448  ntrivcvgmul  14634  prodmo  14666  iscatd2  16342  gictr  17717  gsumval3eu  18305  ptbasin  21380  txcls  21407  txbasval  21409  hmphtr  21586  reconn  22631  phtpcer  22794  phtpcerOLD  22795  pcohtpy  22820  mbfi1flimlem  23489  mbfmullem  23492  itg2add  23526  spc2ed  29312  brabgaf  29420  pconnconn  31213  txsconn  31223  frrlem4  31783  frrlem5c  31786  neibastop1  32354  bj-dtru  32797  riscer  33787  fnchoice  39188  fzisoeu  39514  stoweidlem35  40252  elsprel  41725