Theorem eeanv 1951

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

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

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548

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

This theorem is referenced by:  eeeanv  1952  ee4anv  1953  2eu4  2138  cgsex2g  2799  cgsex4g  2800  vtocl2  2819  spc2egv  2854  spc2gv  2855  dtruarb  4224  copsex2t  4278  copsex2g  4279  opelopabsb  4294  xpmlem  5090  fununi  5326  imain  5340  brabvv  5968  spc2ed  6291  tfrlem7  6375  ener  6838  domtr  6844  unen  6875  mapen  6907  sbthlemi10  7032  ltexprlemdisj  7673  recexprlemdisj  7697  hashfacen  10928  summodc  11548