Theorem 2exbii 1719

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

Syntax hints:   <-> wb 188   E.wex 1663

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

This theorem depends on definitions:  df-bi 189  df-ex 1664

This theorem is referenced by:  3exbii  1720  3exdistr  1839  eeeanv  2079  ee4anv  2080  cbvex4v  2126  2sb5rf  2280  sbel2x  2288  2exsb  2298  2mo2  2379  rexcomf  2950  reean  2957  ceqsex3v  3088  ceqsex4v  3089  ceqsex8v  3091  vtocl3  3103  copsexg  4687  opelopabsbALT  4710  opabn0  4732  rabxp  4871  elxp3  4885  elvv  4893  elvvv  4894  copsex2gb  4945  elcnv2  5012  cnvuni  5021  xpdifid  5265  coass  5354  fununi  5649  dfmpt3  5698  tpres  6117  dfoprab2  6337  dmoprab  6377  rnoprab  6379  mpt2mptx  6387  resoprab  6392  elrnmpt2res  6410  ov3  6433  ov6g  6434  uniuni  6600  oprabex3  6782  wfrlem4  7039  oeeu  7304  xpassen  7666  zorn2lem6  8931  ltresr  9564  axaddf  9569  axmulf  9570  hashfun  12609  hash2prb  12633  5oalem7  27313  mpt2mptxf  28280  eulerpartlemgvv  29209  bnj600  29730  bnj916  29744  bnj983  29762  bnj986  29765  bnj996  29766  bnj1021  29775  elima4  30421  brtxp2  30648  brpprod3a  30653  brpprod3b  30654  elfuns  30682  brcart  30699  brimg  30704  brapply  30705  brsuccf  30708  brrestrict  30716  dfrdg4  30718  ellines  30919  bj-cbvex4vv  31344  itg2addnclem3  31995  dalem20  33258  dvhopellsm  34685  diblsmopel  34739  pm11.52  36736  2exanali  36737  pm11.6  36742  pm11.7  36746  opelopab4  36918  stoweidlem35  37896  mpt2mptx2  40169