Theorem eeanv 1960

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

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

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557

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

This theorem is referenced by:  eeeanv  1961  ee4anv  1962  2eu4  2147  cgsex2g  2808  cgsex4g  2809  vtocl2  2828  spc2egv  2863  spc2gv  2864  dtruarb  4235  copsex2t  4289  copsex2g  4290  opelopabsb  4306  xpmlem  5103  fununi  5342  imain  5356  brabvv  5991  spc2ed  6319  tfrlem7  6403  ener  6871  domtr  6877  unen  6908  mapen  6943  sbthlemi10  7068  ltexprlemdisj  7719  recexprlemdisj  7743  hashfacen  10981  summodc  11694