Theorem eeanv 2218

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

Syntax hints:   ↔ wb 196   ∧ wa 383  ∃wex 1744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ex 1745  df-nf 1750

This theorem is referenced by:  eeeanv  2219  ee4anv  2220  2mo2  2579  cgsex2g  3270  cgsex4g  3271  vtocl2  3292  spc2egv  3326  dtru  4887  copsex2t  4986  copsex2g  4987  xpnz  5588  fununi  6002  wfrlem4  7463  wfrfun  7470  tfrlem7  7524  ener  8044  domtr  8050  unen  8081  undom  8089  sbthlem10  8120  mapen  8165  infxpenc2  8883  fseqen  8888  dfac5lem4  8987  zorn2lem6  9361  fpwwe2lem12  9501  genpnnp  9865  hashfacen  13276  summo  14492  ntrivcvgmul  14678  prodmo  14710  iscatd2  16389  gictr  17764  gsumval3eu  18351  ptbasin  21428  txcls  21455  txbasval  21457  hmphtr  21634  reconn  22678  phtpcer  22841  pcohtpy  22866  mbfi1flimlem  23534  mbfmullem  23537  itg2add  23571  spc2ed  29440  brabgaf  29546  pconnconn  31339  txsconn  31349  frrlem4  31908  frrlem5c  31911  neibastop1  32479  bj-dtru  32922  riscer  33917  br1cosscnvxrn  34364  fnchoice  39502  fzisoeu  39828  stoweidlem35  40570  elsprel  42050