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  4386  opelopabsbALT  4403  opabm  4425  uniuni  4599  rabxp  4814  elxp3  4831  elvv  4839  elvvv  4840  rexiunxp  4924  elcnv2  4960  cnvuni  4968  coass  5309  fununi  5452  dfmpt3  5509  dfoprab2  6138  dmoprab  6172  rnoprab  6174  mpomptx  6182  resoprab  6187  ovi3  6229  ov6g  6230  oprabex3  6366  xpassen  7132  enq0enq  7804  enq0sym  7805  enq0tr  7807  ltresr  8212  axaddf  8241  axmulf  8242