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  2770  reean  2777  ceqsex3v  2897  ceqsex4v  2898  ceqsex8v  2900  vtocl3  2911  axxpprim  4090  elxpk2  4197  elvvk  4207  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opksnelsik  4265  xpkvexg  4285  sikexlem  4295  dfpw12  4301  insklem  4304  ltfinex  4464  ncfinlower  4483  copsexg  4607  copsex4g  4610  opeqexb  4620  opabn0  4716  br1stg  4730  setconslem4  4734  setconslem6  4736  elswap  4740  dfsi2  4751  opelxp  4811  rabxp  4814  elxp3  4831  elcnv2  4890  cnvuni  4895  elres  4995  coass  5097  fununi  5160  cnvswap  5510  cnvsi  5518  dmsi  5519  dfoprab2  5558  dmoprab  5574  rnoprab  5576  resoprab  5581  fnov  5591  ov3  5599  ov6g  5600  mpt2mptx  5708  brtxp  5783  restxp  5786  oqelins4  5794  dmtxp  5802  brpprod  5839  dmpprod  5840  fnpprod  5843  lecex  6115  mucnc  6131  tcdi  6164  ce0nnul  6177  addccan2nclem1  6263