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

Theorem oveqi 6923
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 6916 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1656  (class class class)co 6910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-uni 4661  df-br 4876  df-iota 6090  df-fv 6135  df-ov 6913
This theorem is referenced by:  oveq123i  6924  cantnfval2  8850  vdwap1  16059  vdwlem12  16074  prdsdsval3  16505  oppchom  16734  rcaninv  16813  initoeu2lem0  17022  yonedalem21  17273  yonedalem22  17278  mndprop  17677  issubm  17707  frmdadd  17753  grpprop  17799  oppgplus  18136  ablprop  18564  ringpropd  18943  crngpropd  18944  ringprop  18945  opprmul  18987  opprringb  18993  mulgass3  18998  rngidpropd  19056  invrpropd  19059  drngprop  19121  subrgpropd  19177  rhmpropd  19178  lidlacl  19581  lidlmcl  19585  lidlrsppropd  19598  crngridl  19606  psradd  19750  ressmpladd  19825  ressmplmul  19826  ressmplvsca  19827  ressply1add  19967  ressply1mul  19968  ressply1vsca  19969  ply1coe  20033  scmatscmiddistr  20689  1marepvsma1  20764  decpmatmulsumfsupp  20955  pmatcollpw1lem2  20957  pmatcollpwscmatlem1  20971  mptcoe1matfsupp  20984  mp2pm2mplem4  20991  chmatval  21011  chpidmat  21029  xpsdsval  22563  blres  22613  nmfval2  22772  nmval2  22773  ngpocelbl  22885  cncfmet  23088  ehl1eudisval  23596  ehl2eudisval  23598  minveclem2  23601  minveclem3b  23603  minveclem4  23607  minveclem6  23609  ply1divalg2  24304  clwwlknon1  27468  clwwlknon1nloop  27470  clwwlknon2  27473  nvm  28047  madjusmdetlem1  30434  xrge0pluscn  30527  esumpfinvallem  30677  ptrecube  33952  equivbnd2  34132  ismtyres  34148  iccbnd  34180  exidreslem  34217  iscrngo2  34337  toycom  35047  mendplusgfval  38597  sge0tsms  41386  vonn0ioo  41693  vonn0icc  41694  issubmgm  42654  rhmsubclem4  42954  zlmodzxzadd  43001  snlindsntor  43125
  Copyright terms: Public domain W3C validator