Theorem 2exbii 1655

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

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

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 1496  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1656  19.42vvvv  1965  3exdistr  1967  cbvex4v  1986  ee4anv  1990  ee8anv  1991  sbel2x  2054  2eu4  2176  rexcomf  2707  reean  2714  ceqsex3v  2859  ceqsex4v  2860  ceqsex8v  2862  copsexg  4365  opelopabsbALT  4382  opabm  4404  uniuni  4577  rabxp  4792  elxp3  4809  elvv  4817  elvvv  4818  rexiunxp  4902  elcnv2  4938  cnvuni  4946  coass  5286  fununi  5429  dfmpt3  5486  dfoprab2  6108  dmoprab  6142  rnoprab  6144  mpomptx  6152  resoprab  6157  ovi3  6199  ov6g  6200  oprabex3  6335  xpassen  7094  enq0enq  7762  enq0sym  7763  enq0tr  7765  ltresr  8170  axaddf  8199  axmulf  8200