Theorem eeanv 1804

Description: Rearrange existential quantifiers. (Contributed by NM, 26-Jul-1995.)

Assertion

Ref	Expression
eeanv	⊢ (∃x∃y(φ ∧ ψ) ↔ (∃xφ ∧ ∃yψ))

Distinct variable groups:   φ,y   ψ,x

Allowed substitution hints:   φ(x)   ψ(y)

Proof of Theorem eeanv

Step	Hyp	Ref	Expression
1		nfv 1418	. 2 ⊢ Ⅎyφ
2		nfv 1418	. 2 ⊢ Ⅎxψ
3	1, 2	eean 1803	1 ⊢ (∃x∃y(φ ∧ ψ) ↔ (∃xφ ∧ ∃yψ))

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

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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424

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

This theorem is referenced by:  eeeanv  1805  ee4anv  1806  2eu4  1990  cgsex2g  2584  cgsex4g  2585  vtocl2  2603  spc2egv  2636  spc2gv  2637  dtruarb  3933  copsex2t  3973  copsex2g  3974  opelopabsb  3988  xpmlem  4687  fununi  4910  imain  4924  brabvv  5493  tfrlem7  5874  ener  6195  domtr  6201  unen  6229  ltexprlemdisj  6580  recexprlemdisj  6602