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  1963  3exdistr  1965  cbvex4v  1984  ee4anv  1988  ee8anv  1989  sbel2x  2052  2eu4  2174  rexcomf  2705  reean  2712  ceqsex3v  2857  ceqsex4v  2858  ceqsex8v  2860  copsexg  4360  opelopabsbALT  4377  opabm  4399  uniuni  4572  rabxp  4787  elxp3  4804  elvv  4812  elvvv  4813  rexiunxp  4897  elcnv2  4933  cnvuni  4941  coass  5281  fununi  5424  dfmpt3  5481  dfoprab2  6100  dmoprab  6134  rnoprab  6136  mpomptx  6144  resoprab  6149  ovi3  6191  ov6g  6192  oprabex3  6322  xpassen  7081  enq0enq  7746  enq0sym  7747  enq0tr  7749  ltresr  8154  axaddf  8183  axmulf  8184