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

Theorem oveqi 6283
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 6276 . 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 1398  (class class class)co 6270
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2810  df-uni 4236  df-br 4440  df-iota 5534  df-fv 5578  df-ov 6273
This theorem is referenced by:  oveq123i  6284  cantnfval2  8079  cantnfval2OLD  8109  vdwap1  14582  vdwlem12  14597  prdsdsval3  14977  oppchom  15206  rcaninv  15285  initoeu2lem0  15494  yonedalem21  15744  yonedalem22  15749  mndprop  16149  issubm  16180  frmdadd  16225  grpprop  16271  oppgplus  16586  ablprop  17011  ringpropd  17428  crngpropd  17429  ringprop  17430  opprmul  17473  opprringb  17479  mulgass3  17484  rngidpropd  17542  invrpropd  17545  drngprop  17605  subrgpropd  17661  rhmpropd  17662  lidlacl  18058  lidlmcl  18063  lidlrsppropd  18076  crngridl  18084  psradd  18233  ressmpladd  18317  ressmplmul  18318  ressmplvsca  18319  ressply1add  18469  ressply1mul  18470  ressply1vsca  18471  ply1coe  18535  ply1coeOLD  18536  scmatscmiddistr  19180  1marepvsma1  19255  decpmatmulsumfsupp  19444  pmatcollpw1lem2  19446  pmatcollpwscmatlem1  19460  mptcoe1matfsupp  19473  mp2pm2mplem4  19480  chmatval  19500  chpidmat  19518  xpsdsval  21053  blres  21103  nmfval2  21280  nmval2  21281  cncfmet  21581  minveclem2  22010  minveclem3b  22012  minveclem4  22016  minveclem6  22018  ply1divalg2  22708  issubgoi  25513  ghgrplem2OLD  25570  nvm  25737  xrge0pluscn  28160  esumpfinvallem  28306  equivbnd2  30531  ismtyres  30547  iccbnd  30579  exidreslem  30582  iscrngo2  30638  mendplusgfval  31378  issubmgm  32868  rhmsubclem4  33170  zlmodzxzadd  33220  snlindsntor  33345  toycom  35114
  Copyright terms: Public domain W3C validator