Theorem 2exbii 1628

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

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

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-ial 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1629  19.42vvvv  1936  3exdistr  1938  cbvex4v  1957  ee4anv  1961  ee8anv  1962  sbel2x  2025  2eu4  2146  rexcomf  2667  reean  2674  ceqsex3v  2814  ceqsex4v  2815  ceqsex8v  2817  copsexg  4287  opelopabsbALT  4303  opabm  4325  uniuni  4496  rabxp  4710  elxp3  4727  elvv  4735  elvvv  4736  rexiunxp  4818  elcnv2  4854  cnvuni  4862  coass  5198  fununi  5336  dfmpt3  5392  dfoprab2  5982  dmoprab  6016  rnoprab  6018  mpomptx  6026  resoprab  6031  ovi3  6073  ov6g  6074  oprabex3  6204  xpassen  6907  enq0enq  7526  enq0sym  7527  enq0tr  7529  ltresr  7934  axaddf  7963  axmulf  7964