Theorem 2exbii 1599

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

Hypothesis

Ref	Expression
exbii.1	|- ( ph <-> ps )

Assertion

Ref	Expression
2exbii	|- ( E. x E. y ph <-> E. x E. y ps )

Proof of Theorem 2exbii

Step	Hyp	Ref	Expression
1		exbii.1	. . 3 |- ( ph <-> ps )
2	1	exbii 1598	. 2 |- ( E. y ph <-> E. y ps )
3	2	exbii 1598	1 |- ( E. x E. y ph <-> E. x E. y ps )

Syntax hints:   <-> wb 104   E.wex 1485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3exbii  1600  19.42vvvv  1906  3exdistr  1908  cbvex4v  1923  ee4anv  1927  ee8anv  1928  sbel2x  1991  2eu4  2112  rexcomf  2632  reean  2638  ceqsex3v  2772  ceqsex4v  2773  ceqsex8v  2775  copsexg  4227  opelopabsbALT  4242  opabm  4263  uniuni  4434  rabxp  4646  elxp3  4663  elvv  4671  elvvv  4672  rexiunxp  4751  elcnv2  4787  cnvuni  4795  coass  5127  fununi  5264  dfmpt3  5318  dfoprab2  5897  dmoprab  5931  rnoprab  5933  mpomptx  5941  resoprab  5946  ovi3  5986  ov6g  5987  oprabex3  6105  xpassen  6804  enq0enq  7380  enq0sym  7381  enq0tr  7383  ltresr  7788  axaddf  7817  axmulf  7818