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

Theorem oveqi 6099
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 6092 . 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 1369  (class class class)co 6086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089
This theorem is referenced by:  oveq123i  6100  cantnfval2  7869  cantnfval2OLD  7899  vdwap1  14030  vdwlem12  14045  prdsdsval3  14415  oppchom  14646  yonedalem21  15075  yonedalem22  15080  mndprop  15440  issubm  15466  frmdadd  15524  grpprop  15548  oppgplus  15855  ablprop  16279  rngpropd  16664  crngpropd  16665  rngprop  16666  opprmul  16706  opprrngb  16712  mulgass3  16717  rngidpropd  16775  invrpropd  16778  drngprop  16821  subrgpropd  16877  rhmpropd  16878  lidlacl  17272  lidlmcl  17276  lidlrsppropd  17289  crngridl  17297  psradd  17430  ressmpladd  17513  ressmplmul  17514  ressmplvsca  17515  ressply1add  17659  ressply1mul  17660  ressply1vsca  17661  ply1coe  17721  ply1coeOLD  17722  1marepvsma1  18369  xpsdsval  19931  blres  19981  nmfval2  20158  nmval2  20159  cncfmet  20459  minveclem2  20888  minveclem3b  20890  minveclem4  20894  minveclem6  20896  ply1divalg2  21585  issubgoi  23748  ghgrplem2  23805  nvm  23972  xrge0pluscn  26322  esumpfinvallem  26475  equivbnd2  28644  ismtyres  28660  iccbnd  28692  exidreslem  28695  iscrngo2  28751  mendplusgfval  29495  zlmodzxzadd  30706  pmatcollpw1lem5  30818  snlindsntor  30894  toycom  32458
  Copyright terms: Public domain W3C validator