Theorem 2exbii 1593

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

Syntax hints:   <-> wb 104   E.wex 1479

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1434  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-ial 1521

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3exbii  1594  19.42vvvv  1900  3exdistr  1902  cbvex4v  1917  ee4anv  1921  ee8anv  1922  sbel2x  1985  2eu4  2106  rexcomf  2626  reean  2632  ceqsex3v  2763  ceqsex4v  2764  ceqsex8v  2766  copsexg  4216  opelopabsbALT  4231  opabm  4252  uniuni  4423  rabxp  4635  elxp3  4652  elvv  4660  elvvv  4661  rexiunxp  4740  elcnv2  4776  cnvuni  4784  coass  5116  fununi  5250  dfmpt3  5304  dfoprab2  5880  dmoprab  5914  rnoprab  5916  mpomptx  5924  resoprab  5929  ovi3  5969  ov6g  5970  oprabex3  6089  xpassen  6787  enq0enq  7363  enq0sym  7364  enq0tr  7366  ltresr  7771  axaddf  7800  axmulf  7801