MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oveqi Structured version   Visualization version   GIF version

Theorem oveqi 6623
Description: Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
Hypothesis
Ref Expression
oveq1i.1 𝐴 = 𝐵
Assertion
Ref Expression
oveqi (𝐶𝐴𝐷) = (𝐶𝐵𝐷)

Proof of Theorem oveqi
StepHypRef Expression
1 oveq1i.1 . 2 𝐴 = 𝐵
2 oveq 6616 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  (class class class)co 6610
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-rex 2913  df-uni 4408  df-br 4619  df-iota 5815  df-fv 5860  df-ov 6613
This theorem is referenced by:  oveq123i  6624  cantnfval2  8518  vdwap1  15616  vdwlem12  15631  prdsdsval3  16077  oppchom  16307  rcaninv  16386  initoeu2lem0  16595  yonedalem21  16845  yonedalem22  16850  mndprop  17249  issubm  17279  frmdadd  17324  grpprop  17370  oppgplus  17711  ablprop  18136  ringpropd  18514  crngpropd  18515  ringprop  18516  opprmul  18558  opprringb  18564  mulgass3  18569  rngidpropd  18627  invrpropd  18630  drngprop  18690  subrgpropd  18746  rhmpropd  18747  lidlacl  19145  lidlmcl  19149  lidlrsppropd  19162  crngridl  19170  psradd  19314  ressmpladd  19389  ressmplmul  19390  ressmplvsca  19391  ressply1add  19532  ressply1mul  19533  ressply1vsca  19534  ply1coe  19598  scmatscmiddistr  20246  1marepvsma1  20321  decpmatmulsumfsupp  20510  pmatcollpw1lem2  20512  pmatcollpwscmatlem1  20526  mptcoe1matfsupp  20539  mp2pm2mplem4  20546  chmatval  20566  chpidmat  20584  xpsdsval  22109  blres  22159  nmfval2  22318  nmval2  22319  ngpocelbl  22431  cncfmet  22634  minveclem2  23120  minveclem3b  23122  minveclem4  23126  minveclem6  23128  ply1divalg2  23819  nvm  27366  madjusmdetlem1  29699  xrge0pluscn  29792  esumpfinvallem  29941  ptrecube  33076  equivbnd2  33258  ismtyres  33274  iccbnd  33306  exidreslem  33343  iscrngo2  33463  toycom  33775  mendplusgfval  37271  sge0tsms  39930  vonn0ioo  40234  vonn0icc  40235  issubmgm  41103  rhmsubclem4  41403  zlmodzxzadd  41450  snlindsntor  41574
  Copyright terms: Public domain W3C validator