Theorem 2exbii 1683

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

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

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

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

This theorem is referenced by:  3exbii  1684  3exdistr  1798  eeeanv  2007  ee4anv  2008  cbvex4v  2050  2sb5rf  2209  sbel2x  2217  2exsb  2227  2mo2  2313  2moOLD  2315  2eu4OLD  2322  2eu6OLD  2325  rexcomf  2955  reean  2962  ceqsex3v  3087  ceqsex4v  3088  ceqsex8v  3090  vtocl3  3101  copsexg  4660  opelopabsbALT  4683  opabn0  4705  rabxp  4963  elxp3  4977  elvv  4985  elvvv  4986  copsex2gb  5039  elcnv2  5106  cnvuni  5115  xpdifid  5358  coass  5447  fununi  5575  dfmpt3  5624  tpres  6040  dfoprab2  6260  dmoprab  6300  rnoprab  6302  mpt2mptx  6310  resoprab  6315  elrnmpt2res  6333  ov3  6356  ov6g  6357  uniuni  6526  oprabex3  6706  oeeu  7188  xpassen  7548  zorn2lem6  8812  ltresr  9446  axaddf  9451  axmulf  9452  hashfun  12418  5oalem7  26716  mpt2mptxf  27695  eulerpartlemgvv  28534  elima4  29410  wfrlem4  29547  brtxp2  29720  brpprod3a  29725  brpprod3b  29726  elfuns  29754  brcart  29771  brimg  29776  brapply  29777  brsuccf  29780  brrestrict  29788  dfrdg4  29789  ellines  29991  itg2addnclem3  30270  pm11.52  31496  2exanali  31497  pm11.6  31502  pm11.7  31506  stoweidlem35  32018  mpt2mptx2  33159  opelopab4  33699  bnj600  34359  bnj916  34373  bnj983  34391  bnj986  34394  bnj996  34395  bnj1021  34404  bj-cbvex4vv  34690  dalem20  35865  dvhopellsm  37292  diblsmopel  37346