Theorem eeanv 1959

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

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

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-17 1548  ax-ial 1556

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

This theorem is referenced by:  eeeanv  1960  ee4anv  1961  2eu4  2146  cgsex2g  2807  cgsex4g  2808  vtocl2  2827  spc2egv  2862  spc2gv  2863  dtruarb  4234  copsex2t  4288  copsex2g  4289  opelopabsb  4305  xpmlem  5102  fununi  5341  imain  5355  brabvv  5990  spc2ed  6318  tfrlem7  6402  ener  6870  domtr  6876  unen  6907  mapen  6942  sbthlemi10  7067  ltexprlemdisj  7718  recexprlemdisj  7742  hashfacen  10979  summodc  11636