Theorem 2exbii 1645

Description: Inference adding two existential quantifiers to both sides of an equivalence. (Contributed by NM, 16-Mar-1995.)

Hypothesis

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

Syntax hints:   <-> wb 184   E.wex 1596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612

This theorem depends on definitions:  df-bi 185  df-ex 1597

This theorem is referenced by:  3exbii  1646  3exdistr  1954  eeeanv  1958  ee4anv  1959  cbvex4v  2007  2sb5rf  2181  sbel2x  2191  sbel2xOLD  2192  2exsb  2204  2mo2  2381  2moOLD  2383  2eu4OLD  2391  2eu6OLD  2394  rexcomf  3026  reean  3033  ceqsex3v  3158  ceqsex4v  3159  ceqsex8v  3161  vtocl3  3172  copsexg  4738  copsexgOLD  4739  opelopabsbALT  4762  opabn0  4784  rabxp  5042  elxp3  5056  elvv  5064  elvvv  5065  copsex2gb  5119  elcnv2  5186  cnvuni  5195  xpdifid  5441  coass  5532  fununi  5660  dfmpt3  5709  dfoprab2  6338  dmoprab  6378  rnoprab  6380  mpt2mptx  6388  resoprab  6393  elrnmpt2res  6411  ov3  6434  ov6g  6435  uniuni  6604  oprabex3  6784  oeeu  7264  xpassen  7623  zorn2lem6  8893  ltresr  9529  axaddf  9534  axmulf  9535  hashfun  12476  5oalem7  26401  mpt2mptxf  27341  eulerpartlemgvv  28140  elima4  29136  wfrlem4  29273  brtxp2  29458  brpprod3a  29463  brpprod3b  29464  elfuns  29492  brcart  29509  brimg  29514  brapply  29515  brsuccf  29518  brrestrict  29526  dfrdg4  29527  ellines  29729  itg2addnclem3  29995  pm11.52  31194  2exanali  31195  pm11.6  31200  pm11.7  31204  stoweidlem35  31658  mpt2mptx2  32403  opelopab4  32805  bnj600  33457  bnj916  33471  bnj983  33489  bnj986  33492  bnj996  33493  bnj1021  33502  bj-cbvex4vv  33791  dalem20  34890  dvhopellsm  36315  diblsmopel  36369