Theorem 2exbii 1635

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

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

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

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

This theorem is referenced by:  3exbii  1636  3exdistr  1927  eeeanv  1931  ee4anv  1932  cbvex4v  1981  2sb5rf  2161  sbel2x  2171  sbel2xOLD  2172  2exsb  2183  2eu4  2361  2eu6  2363  rexcomf  2870  reean  2877  ceqsex3v  3001  ceqsex4v  3002  ceqsex8v  3004  vtocl3  3015  copsexg  4564  copsexgOLD  4565  opelopabsbOLD  4586  opabn0  4608  rabxp  4862  elxp3  4876  elvv  4884  elvvv  4885  copsex2gb  4937  elcnv2  5004  cnvuni  5013  xpdifid  5254  coass  5344  fununi  5472  dfmpt3  5521  dfoprab2  6122  dmoprab  6160  rnoprab  6162  mpt2mptx  6170  resoprab  6175  elrnmpt2res  6193  ov3  6216  ov6g  6217  uniuni  6374  oprabex3  6555  oeeu  7030  xpassen  7393  zorn2lem6  8658  ltresr  9295  axaddf  9300  axmulf  9301  hashfun  12183  5oalem7  24886  mpt2mptxf  25819  eulerpartlemgvv  26607  elima4  27437  wfrlem4  27574  brtxp2  27759  brpprod3a  27764  brpprod3b  27765  elfuns  27793  brcart  27810  brimg  27815  brapply  27816  brsuccf  27819  brrestrict  27827  dfrdg4  27828  ellines  28030  itg2addnclem3  28289  pm11.52  29484  2exanali  29485  pm11.6  29490  pm11.7  29494  stoweidlem35  29676  mpt2mptx2  30569  opelopab4  30961  bnj600  31614  bnj916  31628  bnj983  31646  bnj986  31649  bnj996  31650  bnj1021  31659  bj-cbvex4vv  31875  dalem20  32910  dvhopellsm  34335  diblsmopel  34389