Theorem eeanv 1855

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

Syntax hints:   ∧ wa 102   ↔ wb 103  ∃wex 1426

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-4 1445  ax-17 1464  ax-ial 1472

This theorem depends on definitions:  df-bi 115  df-nf 1395

This theorem is referenced by:  eeeanv  1856  ee4anv  1857  2eu4  2041  cgsex2g  2655  cgsex4g  2656  vtocl2  2674  spc2egv  2708  spc2gv  2709  dtruarb  4026  copsex2t  4072  copsex2g  4073  opelopabsb  4087  xpmlem  4852  fununi  5082  imain  5096  brabvv  5695  spc2ed  5998  tfrlem7  6082  ener  6494  domtr  6500  unen  6531  mapen  6560  sbthlemi10  6673  ltexprlemdisj  7163  recexprlemdisj  7187  hashfacen  10237  isummo  10769