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  1962  3exdistr  1964  cbvex4v  1983  ee4anv  1987  ee8anv  1988  sbel2x  2051  2eu4  2173  rexcomf  2696  reean  2703  ceqsex3v  2847  ceqsex4v  2848  ceqsex8v  2850  copsexg  4342  opelopabsbALT  4359  opabm  4381  uniuni  4554  rabxp  4769  elxp3  4786  elvv  4794  elvvv  4795  rexiunxp  4878  elcnv2  4914  cnvuni  4922  coass  5262  fununi  5405  dfmpt3  5462  dfoprab2  6078  dmoprab  6112  rnoprab  6114  mpomptx  6122  resoprab  6127  ovi3  6169  ov6g  6170  oprabex3  6300  xpassen  7057  enq0enq  7694  enq0sym  7695  enq0tr  7697  ltresr  8102  axaddf  8131  axmulf  8132