Theorem eeanv 1986

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

Syntax hints:   ∧ wa 104   ↔ wb 105  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583

This theorem depends on definitions:  df-bi 117  df-nf 1510

This theorem is referenced by:  eeeanv  1987  ee4anv  1988  2eu4  2174  cgsex2g  2850  cgsex4g  2851  vtocl2  2870  spc2egv  2907  spc2gv  2908  dtruarb  4304  copsex2t  4361  copsex2g  4362  opelopabsb  4378  xpmlem  5183  fununi  5424  imain  5438  brabvv  6099  spc2ed  6429  tfrlem7  6548  ener  7019  domtr  7025  unen  7058  mapen  7099  sbthlemi10  7236  ltexprlemdisj  7921  recexprlemdisj  7945  hashfacen  11208  summodc  12069