Theorem eeanv 1961

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

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

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558

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

This theorem is referenced by:  eeeanv  1962  ee4anv  1963  2eu4  2148  cgsex2g  2810  cgsex4g  2811  vtocl2  2830  spc2egv  2867  spc2gv  2868  dtruarb  4246  copsex2t  4302  copsex2g  4303  opelopabsb  4319  xpmlem  5117  fununi  5356  imain  5370  brabvv  6009  spc2ed  6337  tfrlem7  6421  ener  6889  domtr  6895  unen  6927  mapen  6963  sbthlemi10  7089  ltexprlemdisj  7749  recexprlemdisj  7773  hashfacen  11013  summodc  11779