Theorem 2exbii 1628

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

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

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 1469  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-4 1532  ax-ial 1556

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  3exbii  1629  19.42vvvv  1936  3exdistr  1938  cbvex4v  1957  ee4anv  1961  ee8anv  1962  sbel2x  2025  2eu4  2146  rexcomf  2667  reean  2674  ceqsex3v  2814  ceqsex4v  2815  ceqsex8v  2817  copsexg  4287  opelopabsbALT  4304  opabm  4326  uniuni  4497  rabxp  4711  elxp3  4728  elvv  4736  elvvv  4737  rexiunxp  4819  elcnv2  4855  cnvuni  4863  coass  5200  fununi  5341  dfmpt3  5397  dfoprab2  5991  dmoprab  6025  rnoprab  6027  mpomptx  6035  resoprab  6040  ovi3  6082  ov6g  6083  oprabex3  6213  xpassen  6924  enq0enq  7543  enq0sym  7544  enq0tr  7546  ltresr  7951  axaddf  7980  axmulf  7981