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 )

This proof depends on syntax axioms:   <-> wb 105   E.wex 1545

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used 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  4384  opelopabsbALT  4401  opabm  4423  uniuni  4597  rabxp  4812  elxp3  4829  elvv  4837  elvvv  4838  rexiunxp  4922  elcnv2  4958  cnvuni  4966  coass  5306  fununi  5449  dfmpt3  5506  dfoprab2  6135  dmoprab  6169  rnoprab  6171  mpomptx  6179  resoprab  6184  ovi3  6226  ov6g  6227  oprabex3  6362  xpassen  7128  enq0enq  7798  enq0sym  7799  enq0tr  7801  ltresr  8206  axaddf  8235  axmulf  8236