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

Theorem oveqi 7371
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 7364 . 2 (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
31, 2ax-mp 5 1 (𝐶𝐴𝐷) = (𝐶𝐵𝐷)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  (class class class)co 7358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-in 3918  df-ss 3928  df-uni 4867  df-br 5107  df-iota 6449  df-fv 6505  df-ov 7361
This theorem is referenced by:  oveq123i  7372  fvmpopr2d  7517  cantnfval2  9606  vdwap1  16850  vdwlem12  16865  prdsdsval3  17368  oppchom  17597  rcaninv  17678  initoeu2lem0  17900  yonedalem21  18163  yonedalem22  18168  mndprop  18583  issubm  18615  frmdadd  18666  smndex1sgrp  18719  smndex1mnd  18721  grpprop  18767  oppgplus  19128  ablprop  19576  ringpropd  20007  crngpropd  20008  ringprop  20009  opprmul  20053  opprringb  20062  mulgass3  20067  rngidpropd  20125  invrpropd  20128  drngprop  20200  subrgpropd  20260  rhmpropd  20261  lidlacl  20686  lidlmcl  20690  lidlrsppropd  20703  crngridl  20711  psradd  21353  ressmpladd  21433  ressmplmul  21434  ressmplvsca  21435  ressply1add  21604  ressply1mul  21605  ressply1vsca  21606  ply1coe  21670  scmatscmiddistr  21860  1marepvsma1  21935  decpmatmulsumfsupp  22125  pmatcollpw1lem2  22127  pmatcollpwscmatlem1  22141  mptcoe1matfsupp  22154  mp2pm2mplem4  22161  chmatval  22181  chpidmat  22199  xpsdsval  23737  blres  23787  nmfval0  23949  nmval2  23951  ngpocelbl  24071  cncfmet  24275  ehl2eudisval  24790  minveclem2  24793  minveclem3b  24795  minveclem4  24799  minveclem6  24801  ply1divalg2  25506  clwwlknon1  29044  clwwlknon1nloop  29046  clwwlknon2  29049  nvm  29586  evls1addd  32276  evls1muld  32277  madjusmdetlem1  32411  xrge0pluscn  32524  esumpfinvallem  32676  ptrecube  36081  equivbnd2  36254  ismtyres  36270  iccbnd  36302  exidreslem  36339  iscrngo2  36459  toycom  37438  frlmsnic  40731  mendplusgfval  41515  sge0tsms  44628  vonn0ioo  44935  vonn0icc  44936  issubmgm  46090  rhmsubclem4  46394  zlmodzxzadd  46441  snlindsntor  46559  indthinc  47079  indthincALT  47080  prsthinc  47081  mndtchom  47117
  Copyright terms: Public domain W3C validator