Theorem 2exbii 1653

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

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

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

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

This theorem is referenced by:  3exbii  1654  3exdistr  1764  eeeanv  1973  ee4anv  1974  cbvex4v  2018  2sb5rf  2179  sbel2x  2187  2exsb  2197  2mo2  2356  2moOLD  2358  2eu4OLD  2365  2eu6OLD  2368  rexcomf  3001  reean  3008  ceqsex3v  3133  ceqsex4v  3134  ceqsex8v  3136  vtocl3  3147  copsexg  4719  copsexgOLD  4720  opelopabsbALT  4743  opabn0  4765  rabxp  5023  elxp3  5037  elvv  5045  elvvv  5046  copsex2gb  5100  elcnv2  5167  cnvuni  5176  xpdifid  5422  coass  5513  fununi  5641  dfmpt3  5690  dfoprab2  6325  dmoprab  6365  rnoprab  6367  mpt2mptx  6375  resoprab  6380  elrnmpt2res  6398  ov3  6421  ov6g  6422  uniuni  6591  oprabex3  6771  oeeu  7251  xpassen  7610  zorn2lem6  8881  ltresr  9517  axaddf  9522  axmulf  9523  hashfun  12471  5oalem7  26447  mpt2mptxf  27387  eulerpartlemgvv  28185  elima4  29181  wfrlem4  29318  brtxp2  29503  brpprod3a  29508  brpprod3b  29509  elfuns  29537  brcart  29554  brimg  29559  brapply  29560  brsuccf  29563  brrestrict  29571  dfrdg4  29572  ellines  29774  itg2addnclem3  30040  pm11.52  31243  2exanali  31244  pm11.6  31249  pm11.7  31253  stoweidlem35  31706  tpres  32390  mpt2mptx2  32652  opelopab4  33052  bnj600  33705  bnj916  33719  bnj983  33737  bnj986  33740  bnj996  33741  bnj1021  33750  bj-cbvex4vv  34043  dalem20  35140  dvhopellsm  36567  diblsmopel  36621