Theorem oveqd 6102

Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveqd	⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Proof of Theorem oveqd

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq 6091	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

This proof depends on syntax axioms:   → wi 4   = wceq 1402  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq123d  6106  oveqdr  6113  csbov12g  6125  ovmpodxf  6214  oprssov  6231  ofeqd  6304  ofeq  6305  fnmpoovd  6451  seqeq2  10890  imasex  13628  imasival  13629  plusffvalg  13684  mgm1  13692  grpidvalg  13695  grpidd  13705  gzsumress  13714  sgrp1  13728  issgrpd  13729  ismndd  13752  issubmnd  13757  mnd1  13764  ismhm  13770  mhmex  13771  issubm  13781  resmhm  13796  resmhm2  13797  resmhm2b  13798  isgrp  13813  isgrpd2e  13827  grpidd2  13848  grpinvfvalg  13849  grp1  13913  imasgrp2  13915  imasgrp  13916  subg0  13985  subginv  13986  subgcl  13989  issubgrpd2  13995  isnsg  14007  nmznsg  14018  isghm  14048  resghm  14065  iscmn  14098  iscmnd  14103  cmnsubm  14114  imasabl  14142  prdsex  14174  prdsval  14175  pwsplusgval  14210  pwsmulrval  14211  rngass  14240  rngcl  14245  rngpropd  14256  dfur2g  14268  issrg  14271  srgcl  14276  srgass  14277  srgideu  14278  issrgid  14287  srgpcomp  14296  srgpcompp  14297  isring  14306  ringcl  14319  crngcom  14320  iscrng2  14321  ringass  14322  ringideu  14323  isringid  14332  ringidss  14336  ringpropd  14345  ring1  14366  opprmulg  14378  oppr0g  14389  oppr1g  14390  opprnegg  14391  mulgass3  14393  dvdsrvald  14402  dvdsrd  14403  opprunitd  14419  dvrvald  14443  rdivmuldivd  14453  rhmmul  14473  isrhm2d  14474  rhmopp  14485  rhmunitinv  14487  islring  14501  lringuplu  14505  opprlring  14506  subrngmcl  14519  subrg1  14541  subrgmcl  14543  subrgdvds  14545  subrguss  14546  subrginv  14547  subrgdv  14548  subrgunit  14549  subrgugrp  14550  issubrg3  14557  rhmpropd  14564  rrgval  14572  aprval  14593  aprap  14600  aprprop  14603  islmod  14629  islmodd  14631  scaffvalg  14645  lmodpropd  14688  lsssetm  14695  islssmd  14698  islidlm  14818  lidlacl  14823  rnglidlmmgm  14835  rnglidlmsgrp  14836  rnglidlrng  14837  rspsn  14873  isassa  15004  isassad  15013  assamulgscmlem2  15044  psrval  15052  psradd  15072  mpladd  15097  blfvalps  15488  lgseisenlem3  16203  lgseisenlem4  16204