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

Theorem oveqi 6295
Description: Equality inference for operation value. (Contributed by NM, 24-Nov-2007.)
Hypothesis
Ref Expression
oveq1i.1  |-  A  =  B
Assertion
Ref Expression
oveqi  |-  ( C A D )  =  ( C B D )

Proof of Theorem oveqi
StepHypRef Expression
1 oveq1i.1 . 2  |-  A  =  B
2 oveq 6288 . 2  |-  ( A  =  B  ->  ( C A D )  =  ( C B D ) )
31, 2ax-mp 5 1  |-  ( C A D )  =  ( C B D )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379  (class class class)co 6282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rex 2820  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285
This theorem is referenced by:  oveq123i  6296  cantnfval2  8084  cantnfval2OLD  8114  vdwap1  14350  vdwlem12  14365  prdsdsval3  14736  oppchom  14967  yonedalem21  15396  yonedalem22  15401  mndprop  15761  issubm  15788  frmdadd  15846  grpprop  15870  oppgplus  16179  ablprop  16605  rngpropd  17017  crngpropd  17018  rngprop  17019  opprmul  17059  opprrngb  17065  mulgass3  17070  rngidpropd  17128  invrpropd  17131  drngprop  17190  subrgpropd  17246  rhmpropd  17247  lidlacl  17643  lidlmcl  17647  lidlrsppropd  17660  crngridl  17668  psradd  17806  ressmpladd  17890  ressmplmul  17891  ressmplvsca  17892  ressply1add  18042  ressply1mul  18043  ressply1vsca  18044  ply1coe  18108  ply1coeOLD  18109  scmatscmiddistr  18777  1marepvsma1  18852  decpmatmulsumfsupp  19041  pmatcollpw1lem2  19043  pmatcollpwscmatlem1  19057  mptcoe1matfsupp  19070  mp2pm2mplem4  19077  chmatval  19097  chpidmat  19115  xpsdsval  20619  blres  20669  nmfval2  20846  nmval2  20847  cncfmet  21147  minveclem2  21576  minveclem3b  21578  minveclem4  21582  minveclem6  21584  ply1divalg2  22274  issubgoi  24988  ghgrplem2  25045  nvm  25212  xrge0pluscn  27558  esumpfinvallem  27720  equivbnd2  29891  ismtyres  29907  iccbnd  29939  exidreslem  29942  iscrngo2  29998  mendplusgfval  30739  zlmodzxzadd  32011  snlindsntor  32145  toycom  33770
  Copyright terms: Public domain W3C validator