MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveq12i Unicode version

Theorem oveq12i 6308
Description: Equality inference for operation value. (Contributed by NM, 28-Feb-1995.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Hypotheses
Ref Expression
oveq1i.1
oveq12i.2
Assertion
Ref Expression
oveq12i

Proof of Theorem oveq12i
StepHypRef Expression
1 oveq1i.1 . 2
2 oveq12i.2 . 2
3 oveq12 6305 . 2
41, 2, 3mp2an 672 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395  (class class class)co 6296
This theorem is referenced by:  oveq123i  6310  caovdir  6509  caovdilem  6510  caovlem2  6511  cnfcom2  8167  cnfcom2OLD  8175  canthwelem  9049  adderpqlem  9353  addassnq  9357  distrnq  9360  ltanq  9370  1lt2nq  9372  ltexnq  9374  halfnq  9375  mulcmpblnrlem  9468  mulcomsr  9487  distrsr  9489  m1p1sr  9490  m1m1sr  9491  mulgt0sr  9503  addcnsrec  9541  mulcnsrec  9542  axmulcom  9553  axmulass  9555  axdistr  9556  axi2m1  9557  addid1  9781  negdiiOLD  9927  3t3e9  10713  8th4div3  10784  halfpm6th  10785  numma  11035  4t3lem  11075  seqfeq4  12156  seqof  12164  sqdivi  12252  i4  12270  binom2i  12277  binom2aiOLD  12278  nn0opthlem1  12348  facp1  12358  fac2  12359  fac3  12360  fac4  12361  faclbnd4lem1  12371  ccat2s1len  12628  ccat2s1p2  12633  cats1len  12825  cji  12992  sqrlem5  13080  fsumadd  13561  fsumsplitsnun  13570  0.999...  13690  fprodmul  13765  fproddiv  13766  efsep  13845  ef01bndlem  13919  cos2bnd  13923  rpnnen2lem3  13950  sadeq  14122  gcdaddmlem  14166  bezout  14180  nn0gcdsq  14285  pythagtriplem16  14354  4sqlem19  14481  dec5nprm  14552  dec2nprm  14553  mod2xnegi  14557  numexp2x  14565  decsplit  14569  karatsuba  14570  2exp16  14575  37prm  14606  43prm  14607  83prm  14608  139prm  14609  163prm  14610  317prm  14611  631prm  14612  1259lem1  14613  1259lem2  14614  1259lem3  14615  1259lem4  14616  1259lem5  14617  1259prm  14618  2503lem1  14619  2503lem2  14620  2503lem3  14621  2503prm  14622  4001lem1  14623  4001lem2  14624  4001lem3  14625  4001lem4  14626  4001prm  14627  funcoppc  15244  yonedalem3b  15548  gsum2dlem2  16998  gsum2dOLD  17000  opprring  17280  isrhm  17370  evlsval  18188  mamudi  18905  mamudir  18906  oftpos  18954  mamutpos  18960  mdetrlin  19104  mdetrlin2  19109  mdetunilem5  19118  cpmadugsumfi  19378  cnmpt2res  20178  ussval  20762  icopnfhmeo  21443  iccpnfhmeo  21445  pcoass  21524  ovolunlem1a  21907  ioombl1lem3  21970  ioombl1lem4  21971  mbfimaopnlem  22062  iblcnlem1  22194  itgfsum  22233  iblabslem  22234  itgsplit  22242  dveflem  22380  efhalfpi  22864  efipi  22866  sin2pi  22868  ef2pi  22870  sincosq3sgn  22893  sincosq4sgn  22894  sinq34lt0t  22902  sincos4thpi  22906  tan4thpi  22907  sincos6thpi  22908  sincos3rdpi  22909  pige3  22910  cxpcn3  23122  lawcos  23148  1cubrlem  23172  quart1lem  23186  quart1  23187  asin1  23225  atancj  23241  atanlogsublem  23246  log2cnv  23275  log2tlbnd  23276  log2ublem3  23279  log2ub  23280  birthday  23284  basellem8  23361  basellem9  23362  cht2  23446  cht3  23447  1sgm2ppw  23475  bclbnd  23555  bposlem8  23566  bposlem9  23567  lgsdi  23607  lgsquadlem1  23629  mirauto  24061  axsegconlem9  24228  ax5seglem7  24238  clwlkfoclwwlk  24845  vdgr0  24900  vdegp1bi  24985  ip0i  25740  ip1ilem  25741  ip2i  25743  ipdirilem  25744  ipasslem10  25754  ip2dii  25759  pythi  25765  siilem1  25766  hvsubsub4i  25976  hvsubcan2i  25981  hisubcomi  26021  normlem0  26026  normlem1  26027  normlem2  26028  normlem3  26029  normlem6  26032  normlem8  26034  normlem9  26035  bcseqi  26037  norm-ii-i  26054  norm-iii-i  26056  normpythi  26059  norm3difi  26064  normpari  26071  normpar2i  26073  polid2i  26074  polidi  26075  bcsiALT  26096  lediri  26455  h1de2i  26471  cmcmlem  26509  cmbr2i  26514  cm2j  26538  fh3i  26541  fh4i  26542  pjaddii  26593  pjsslem  26597  pjssmii  26599  pjdifnormii  26601  lnopeq0lem1  26924  lnopunilem1  26929  lnophmlem2  26936  pjsdi2i  27076  pjclem1  27114  golem1  27190  gsumle  27770  rmulccn  27910  raddcn  27911  xrmulc1cn  27912  xrge0iifhmeo  27918  qqh0  27965  qqh1  27966  elmbfmvol2  28238  mbfmcnt  28239  eulerpartlemgvv  28315  eulerpartlemgh  28317  fib2  28341  fib3  28342  fib4  28343  fib5  28344  fib6  28345  ballotlem2  28427  ballotlemfval0  28434  ballotth  28476  ofs2  28501  signstfveq0  28534  problem2  29020  problem4  29022  quad3  29024  4bc2eq6  29112  halfthird  29113  5recm6rec  29114  bpoly3  29820  fsumcube  29822  iblabsnclem  30078  mzpcompact2lem  30684  pellexlem5  30769  pellfundgt1  30819  jm2.27c  30949  areaquad  31184  lhe4.4ex1a  31234  fsumsplitf  31568  fprodsplitf  31589  mccl  31606  dvnprodlem2  31744  itgsin0pilem1  31748  stoweidlem13  31795  wallispilem4  31850  wallispi2lem1  31853  wallispi2lem2  31854  dirkerper  31878  dirkertrigeqlem1  31880  fourierdlem30  31919  fourierdlem47  31936  fourierdlem103  31992  fourierdlem104  31993  fouriersw  32014  etransclem37  32054  fsumsplitsndif  32346  estrchom  32633  funcestrcsetclem5  32650  2t6m3t4e0  32937  lincsum  33030  zlmodzxzequa  33097  zlmodzxzequap  33100  zlmodzxzldeplem3  33103  dalem10  35397  cdleme0e  35942  cdleme7c  35970  cdleme20c  36037
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6299
  Copyright terms: Public domain W3C validator