Theorem 2exbii 1620

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

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

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 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1621  19.42vvvv  1928  3exdistr  1930  cbvex4v  1949  ee4anv  1953  ee8anv  1954  sbel2x  2017  2eu4  2138  rexcomf  2659  reean  2666  ceqsex3v  2806  ceqsex4v  2807  ceqsex8v  2809  copsexg  4278  opelopabsbALT  4294  opabm  4316  uniuni  4487  rabxp  4701  elxp3  4718  elvv  4726  elvvv  4727  rexiunxp  4809  elcnv2  4845  cnvuni  4853  coass  5189  fununi  5327  dfmpt3  5381  dfoprab2  5970  dmoprab  6004  rnoprab  6006  mpomptx  6014  resoprab  6019  ovi3  6061  ov6g  6062  oprabex3  6187  xpassen  6890  enq0enq  7500  enq0sym  7501  enq0tr  7503  ltresr  7908  axaddf  7937  axmulf  7938