Theorem eeanv 1807

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

Syntax hints:   ∧ wa 97   ↔ wb 98  ∃wex 1381

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427

This theorem depends on definitions:  df-bi 110  df-nf 1350

This theorem is referenced by:  eeeanv  1808  ee4anv  1809  2eu4  1993  cgsex2g  2590  cgsex4g  2591  vtocl2  2609  spc2egv  2642  spc2gv  2643  dtruarb  3942  copsex2t  3982  copsex2g  3983  opelopabsb  3997  xpmlem  4744  fununi  4967  imain  4981  brabvv  5551  tfrlem7  5933  ener  6259  domtr  6265  unen  6293  ltexprlemdisj  6704  recexprlemdisj  6728