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  4277  opelopabsbALT  4293  opabm  4315  uniuni  4486  rabxp  4700  elxp3  4717  elvv  4725  elvvv  4726  rexiunxp  4808  elcnv2  4844  cnvuni  4852  coass  5188  fununi  5326  dfmpt3  5380  dfoprab2  5969  dmoprab  6003  rnoprab  6005  mpomptx  6013  resoprab  6018  ovi3  6060  ov6g  6061  oprabex3  6186  xpassen  6889  enq0enq  7498  enq0sym  7499  enq0tr  7501  ltresr  7906  axaddf  7935  axmulf  7936