Theorem oveqi 6663

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

Step	Hyp	Ref	Expression
1		oveq1i.1	. 2 |- A = B
2		oveq 6656	. 2 |- ( A = B -> ( C A D ) = ( C B D ) )
3	1, 2	ax-mp 5	1 |- ( C A D ) = ( C B D )

Syntax hints:   = wceq 1483  (class class class)co 6650

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653

This theorem is referenced by:  oveq123i  6664  cantnfval2  8566  vdwap1  15681  vdwlem12  15696  prdsdsval3  16145  oppchom  16375  rcaninv  16454  initoeu2lem0  16663  yonedalem21  16913  yonedalem22  16918  mndprop  17317  issubm  17347  frmdadd  17392  grpprop  17438  oppgplus  17779  ablprop  18204  ringpropd  18582  crngpropd  18583  ringprop  18584  opprmul  18626  opprringb  18632  mulgass3  18637  rngidpropd  18695  invrpropd  18698  drngprop  18758  subrgpropd  18814  rhmpropd  18815  lidlacl  19213  lidlmcl  19217  lidlrsppropd  19230  crngridl  19238  psradd  19382  ressmpladd  19457  ressmplmul  19458  ressmplvsca  19459  ressply1add  19600  ressply1mul  19601  ressply1vsca  19602  ply1coe  19666  scmatscmiddistr  20314  1marepvsma1  20389  decpmatmulsumfsupp  20578  pmatcollpw1lem2  20580  pmatcollpwscmatlem1  20594  mptcoe1matfsupp  20607  mp2pm2mplem4  20614  chmatval  20634  chpidmat  20652  xpsdsval  22186  blres  22236  nmfval2  22395  nmval2  22396  ngpocelbl  22508  cncfmet  22711  minveclem2  23197  minveclem3b  23199  minveclem4  23203  minveclem6  23205  ply1divalg2  23898  numclwlk1lem2  27230  nvm  27496  madjusmdetlem1  29893  xrge0pluscn  29986  esumpfinvallem  30136  ptrecube  33409  equivbnd2  33591  ismtyres  33607  iccbnd  33639  exidreslem  33676  iscrngo2  33796  toycom  34260  mendplusgfval  37755  sge0tsms  40597  vonn0ioo  40901  vonn0icc  40902  issubmgm  41789  rhmsubclem4  42089  zlmodzxzadd  42136  snlindsntor  42260