Theorem eeanv 1913

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 1619	. 2 ⊢ Ⅎyφ
2		nfv 1619	. 2 ⊢ Ⅎxψ
3	1, 2	eean 1912	1 ⊢ (∃x∃y(φ ∧ ψ) ↔ (∃xφ ∧ ∃yψ))

Syntax hints:   ↔ wb 176   ∧ wa 358  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542  df-nf 1545

This theorem is referenced by:  eeeanv  1914  ee4anv  1915  pm11.07  2115  2eu4  2287  cgsex2g  2891  cgsex4g  2892  vtocl2  2910  spc2egv  2941  opkelcokg  4261  sikexlem  4295  ncfinlower  4483  sfin112  4529  sfinltfin  4535  copsex2t  4608  copsex2g  4609  opeqexb  4620  opelxp  4811  xpnz  5045  dfxp2  5113  fununi  5160  1stfo  5505  2ndfo  5506  brtxp  5783  dmtxp  5802  dmpprod  5840  pw1fnf1o  5855  entr  6038  fundmen  6043  unen  6048  xpen  6055  muccl  6132  muccom  6134  ncaddccl  6144  ncdisjeq  6148  tcdi  6164  ce0addcnnul  6179  ce0nnulb  6182  ceclb  6183  sbthlem3  6205  dflec3  6221  nclenc  6222  lenc  6223  tc11  6228  ce2le  6233  muc0or  6252  fnfrec  6320