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  6067  spc2ed  6398  tfrlem7  6483  ener  6953  domtr  6959  unen  6991  mapen  7032  sbthlemi10  7165  ltexprlemdisj  7826  recexprlemdisj  7850  hashfacen  11101  summodc  11949