Theorem 2exbii 1630

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

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

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 1471  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1631  19.42vvvv  1938  3exdistr  1940  cbvex4v  1959  ee4anv  1963  ee8anv  1964  sbel2x  2027  2eu4  2148  rexcomf  2669  reean  2676  ceqsex3v  2817  ceqsex4v  2818  ceqsex8v  2820  copsexg  4296  opelopabsbALT  4313  opabm  4335  uniuni  4506  rabxp  4720  elxp3  4737  elvv  4745  elvvv  4746  rexiunxp  4828  elcnv2  4864  cnvuni  4872  coass  5210  fununi  5351  dfmpt3  5408  dfoprab2  6005  dmoprab  6039  rnoprab  6041  mpomptx  6049  resoprab  6054  ovi3  6096  ov6g  6097  oprabex3  6227  xpassen  6940  enq0enq  7564  enq0sym  7565  enq0tr  7567  ltresr  7972  axaddf  8001  axmulf  8002