Theorem 2exbii 1727

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

Syntax hints:   <-> wb 189   E.wex 1671

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

This theorem depends on definitions:  df-bi 190  df-ex 1672

This theorem is referenced by:  3exbii  1728  3exdistr  1847  eeeanv  2094  ee4anv  2095  cbvex4v  2139  2sb5rf  2300  sbel2x  2308  2exsb  2318  2mo2  2399  rexcomf  2936  reean  2943  ceqsex3v  3074  ceqsex4v  3075  ceqsex8v  3077  vtocl3  3089  copsexg  4687  opelopabsbALT  4710  opabn0  4732  rabxp  4876  elxp3  4890  elvv  4898  elvvv  4899  copsex2gb  4950  elcnv2  5017  cnvuni  5026  xpdifid  5271  coass  5361  fununi  5659  dfmpt3  5708  tpres  6133  dfoprab2  6356  dmoprab  6396  rnoprab  6398  mpt2mptx  6406  resoprab  6411  elrnmpt2res  6429  ov3  6452  ov6g  6453  uniuni  6619  oprabex3  6801  wfrlem4  7057  oeeu  7322  xpassen  7684  zorn2lem6  8949  ltresr  9582  axaddf  9587  axmulf  9588  hashfun  12650  hash2prb  12674  5oalem7  27394  mpt2mptxf  28355  eulerpartlemgvv  29282  bnj600  29802  bnj916  29816  bnj983  29834  bnj986  29837  bnj996  29838  bnj1021  29847  elima4  30492  brtxp2  30719  brpprod3a  30724  brpprod3b  30725  elfuns  30753  brcart  30770  brimg  30775  brapply  30776  brsuccf  30779  brrestrict  30787  dfrdg4  30789  ellines  30990  bj-cbvex4vv  31410  itg2addnclem3  32059  dalem20  33329  dvhopellsm  34756  diblsmopel  34810  pm11.52  36806  2exanali  36807  pm11.6  36812  pm11.7  36816  opelopab4  36988  stoweidlem35  38008  mpt2mptx2  40624