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 1577	. 2 ⊢ Ⅎ𝑦𝜑
2		nfv 1577	. 2 ⊢ Ⅎ𝑥𝜓
3	1, 2	eean 1984	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  1986  ee4anv  1987  2eu4  2173  cgsex2g  2840  cgsex4g  2841  vtocl2  2860  spc2egv  2897  spc2gv  2898  dtruarb  4287  copsex2t  4343  copsex2g  4344  opelopabsb  4360  xpmlem  5164  fununi  5405  imain  5419  brabvv  6077  spc2ed  6407  tfrlem7  6526  ener  6996  domtr  7002  unen  7034  mapen  7075  sbthlemi10  7208  ltexprlemdisj  7869  recexprlemdisj  7893  hashfacen  11146  summodc  12007