Theorem 2exbii 1568

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

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

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-ial 1497

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  3exbii  1569  19.42vvvv  1865  3exdistr  1867  cbvex4v  1880  ee4anv  1884  ee8anv  1885  sbel2x  1949  2eu4  2068  rexcomf  2567  reean  2573  ceqsex3v  2699  ceqsex4v  2700  ceqsex8v  2702  copsexg  4126  opelopabsbALT  4141  opabm  4162  uniuni  4332  rabxp  4536  elxp3  4553  elvv  4561  elvvv  4562  rexiunxp  4641  elcnv2  4677  cnvuni  4685  coass  5015  fununi  5149  dfmpt3  5203  dfoprab2  5772  dmoprab  5806  rnoprab  5808  mpomptx  5816  resoprab  5821  ovi3  5861  ov6g  5862  oprabex3  5981  xpassen  6677  enq0enq  7187  enq0sym  7188  enq0tr  7190  ltresr  7574  axaddf  7603  axmulf  7604