Theorem eeanv 2344

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 1995	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1995	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	eean 2343	1 ⊢ (∃𝑥∃𝑦(𝜑 ∧ 𝜓) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝜓))

Syntax hints:   ↔ wb 196   ∧ wa 382  ∃wex 1852

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-10 2174  ax-11 2190  ax-12 2203

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-ex 1853  df-nf 1858

This theorem is referenced by:  eeeanv  2345  ee4anv  2346  2mo2  2699  cgsex2g  3391  cgsex4g  3392  vtocl2  3412  spc2egv  3446  dtru  4988  copsex2t  5084  copsex2g  5085  xpnz  5694  fununi  6104  wfrlem4  7570  wfrlem4OLD  7571  wfrfun  7578  tfrlem7  7632  ener  8156  domtr  8162  unen  8196  undom  8204  sbthlem10  8235  mapen  8280  infxpenc2  9045  fseqen  9050  dfac5lem4  9149  zorn2lem6  9525  fpwwe2lem12  9665  genpnnp  10029  hashfacen  13440  summo  14656  ntrivcvgmul  14841  prodmo  14873  iscatd2  16549  gictr  17925  gsumval3eu  18512  ptbasin  21601  txcls  21628  txbasval  21630  hmphtr  21807  reconn  22851  phtpcer  23014  pcohtpy  23039  mbfi1flimlem  23709  mbfmullem  23712  itg2add  23746  spc2ed  29652  brabgaf  29758  pconnconn  31551  txsconn  31561  frrlem4  32120  frrlem5c  32123  neibastop1  32691  bj-dtru  33133  riscer  34119  br1cosscnvxrn  34566  fnchoice  39710  fzisoeu  40031  stoweidlem35  40769  elsprel  42253