Theorem 2exbii 1585

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

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

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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3exbii  1586  19.42vvvv  1885  3exdistr  1887  cbvex4v  1902  ee4anv  1906  ee8anv  1907  sbel2x  1973  2eu4  2092  rexcomf  2593  reean  2599  ceqsex3v  2728  ceqsex4v  2729  ceqsex8v  2731  copsexg  4166  opelopabsbALT  4181  opabm  4202  uniuni  4372  rabxp  4576  elxp3  4593  elvv  4601  elvvv  4602  rexiunxp  4681  elcnv2  4717  cnvuni  4725  coass  5057  fununi  5191  dfmpt3  5245  dfoprab2  5818  dmoprab  5852  rnoprab  5854  mpomptx  5862  resoprab  5867  ovi3  5907  ov6g  5908  oprabex3  6027  xpassen  6724  enq0enq  7239  enq0sym  7240  enq0tr  7242  ltresr  7647  axaddf  7676  axmulf  7677