Theorem 2exbii 1654

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 1653	. 2 |- ( E. y ph <-> E. y ps )
3	2	exbii 1653	1 |- ( E. x E. y ph <-> E. x E. y ps )

Syntax hints:   <-> wb 105   E.wex 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-ial 1582

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1655  19.42vvvv  1962  3exdistr  1964  cbvex4v  1983  ee4anv  1987  ee8anv  1988  sbel2x  2051  2eu4  2173  rexcomf  2695  reean  2702  ceqsex3v  2846  ceqsex4v  2847  ceqsex8v  2849  copsexg  4336  opelopabsbALT  4353  opabm  4375  uniuni  4548  rabxp  4763  elxp3  4780  elvv  4788  elvvv  4789  rexiunxp  4872  elcnv2  4908  cnvuni  4916  coass  5255  fununi  5398  dfmpt3  5455  dfoprab2  6067  dmoprab  6101  rnoprab  6103  mpomptx  6111  resoprab  6116  ovi3  6158  ov6g  6159  oprabex3  6290  xpassen  7013  enq0enq  7650  enq0sym  7651  enq0tr  7653  ltresr  8058  axaddf  8087  axmulf  8088