Theorem eeanv 1932

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

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

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534

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

This theorem is referenced by:  eeeanv  1933  ee4anv  1934  2eu4  2119  cgsex2g  2775  cgsex4g  2776  vtocl2  2794  spc2egv  2829  spc2gv  2830  dtruarb  4193  copsex2t  4247  copsex2g  4248  opelopabsb  4262  xpmlem  5051  fununi  5286  imain  5300  brabvv  5924  spc2ed  6237  tfrlem7  6321  ener  6782  domtr  6788  unen  6819  mapen  6849  sbthlemi10  6968  ltexprlemdisj  7608  recexprlemdisj  7632  hashfacen  10819  summodc  11394