Theorem 2exbii 1659

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

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

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 1500  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1660  19.42vvvv  1969  3exdistr  1971  cbvex4v  1990  ee4anv  1994  ee8anv  1995  sbel2x  2058  2eu4  2180  rexcomf  2713  reean  2720  ceqsex3v  2865  ceqsex4v  2866  ceqsex8v  2868  copsexg  4379  opelopabsbALT  4396  opabm  4418  uniuni  4592  rabxp  4807  elxp3  4824  elvv  4832  elvvv  4833  rexiunxp  4917  elcnv2  4953  cnvuni  4961  coass  5301  fununi  5444  dfmpt3  5501  dfoprab2  6125  dmoprab  6159  rnoprab  6161  mpomptx  6169  resoprab  6174  ovi3  6216  ov6g  6217  oprabex3  6352  xpassen  7118  enq0enq  7788  enq0sym  7789  enq0tr  7791  ltresr  8196  axaddf  8225  axmulf  8226