Theorem eeanv 1856

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

Syntax hints:   ∧ wa 103   ↔ wb 104  ∃wex 1427

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-4 1446  ax-17 1465  ax-ial 1473

This theorem depends on definitions:  df-bi 116  df-nf 1396

This theorem is referenced by:  eeeanv  1857  ee4anv  1858  2eu4  2042  cgsex2g  2658  cgsex4g  2659  vtocl2  2677  spc2egv  2711  spc2gv  2712  dtruarb  4034  copsex2t  4083  copsex2g  4084  opelopabsb  4098  xpmlem  4867  fununi  5097  imain  5111  brabvv  5711  spc2ed  6014  tfrlem7  6098  ener  6552  domtr  6558  unen  6589  mapen  6618  sbthlemi10  6731  ltexprlemdisj  7228  recexprlemdisj  7252  hashfacen  10304  isummo  10836