Theorem 2exbii 1583

Description: Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)

Hypothesis

Ref	Expression
2exbii.1	⊢ (φ ↔ ψ)

Assertion

Ref	Expression
2exbii	⊢ (∃x∃yφ ↔ ∃x∃yψ)

Proof of Theorem 2exbii

Step	Hyp	Ref	Expression
1		2exbii.1	. . 3 ⊢ (φ ↔ ψ)
2	1	exbii 1582	. 2 ⊢ (∃yφ ↔ ∃yψ)
3	2	exbii 1582	1 ⊢ (∃x∃yφ ↔ ∃x∃yψ)

Syntax hints:   ↔ wb 176  ∃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

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  3exbii  1584  3exdistr  1910  ee4anv  1915  cbvex4v  2012  sbel2x  2125  2eu4  2287  2eu6  2289  rexcomf  2771  reean  2778  ceqsex3v  2898  ceqsex4v  2899  ceqsex8v  2901  vtocl3  2912  axxpprim  4091  elxpk2  4198  elvvk  4208  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opksnelsik  4266  xpkvexg  4286  sikexlem  4296  dfpw12  4302  insklem  4305  ltfinex  4465  ncfinlower  4484  copsexg  4608  copsex4g  4611  opeqexb  4621  opabn0  4717  br1stg  4731  setconslem4  4735  setconslem6  4737  elswap  4741  dfsi2  4752  opelxp  4812  rabxp  4815  elxp3  4832  elcnv2  4891  cnvuni  4896  elres  4996  coass  5098  fununi  5161  cnvswap  5511  cnvsi  5519  dmsi  5520  dfoprab2  5559  dmoprab  5575  rnoprab  5577  resoprab  5582  fnov  5592  ov3  5600  ov6g  5601  mpt2mptx  5709  brtxp  5784  restxp  5787  oqelins4  5795  dmtxp  5803  brpprod  5840  dmpprod  5841  fnpprod  5844  lecex  6116  mucnc  6132  tcdi  6165  ce0nnul  6178  addccan2nclem1  6264