Theorem eeanv 1985

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

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

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582

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

This theorem is referenced by:  eeeanv  1986  ee4anv  1987  2eu4  2173  cgsex2g  2839  cgsex4g  2840  vtocl2  2859  spc2egv  2896  spc2gv  2897  dtruarb  4281  copsex2t  4337  copsex2g  4338  opelopabsb  4354  xpmlem  5157  fununi  5398  imain  5412  brabvv  6066  spc2ed  6397  tfrlem7  6482  ener  6952  domtr  6958  unen  6990  mapen  7031  sbthlemi10  7164  ltexprlemdisj  7825  recexprlemdisj  7849  hashfacen  11099  summodc  11943