Theorem oveqd 6030

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 6019	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝐴𝐷) = (𝐶𝐵𝐷))

Syntax hints:   → wi 4   = wceq 1395  (class class class)co 6013

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  oveq123d  6034  oveqdr  6041  csbov12g  6053  ovmpodxf  6142  oprssov  6159  ofeqd  6232  ofeq  6233  fnmpoovd  6375  seqeq2  10706  prdsex  13345  prdsval  13349  pwsplusgval  13371  pwsmulrval  13372  imasex  13381  imasival  13382  plusffvalg  13438  mgm1  13446  grpidvalg  13449  grpidd  13459  gsumress  13471  sgrp1  13487  issgrpd  13488  ismndd  13513  issubmnd  13518  mnd1  13531  ismhm  13537  mhmex  13538  issubm  13548  resmhm  13563  resmhm2  13564  resmhm2b  13565  isgrp  13582  isgrpd2e  13596  grpidd2  13617  grpinvfvalg  13618  grp1  13682  imasgrp2  13690  imasgrp  13691  subg0  13760  subginv  13761  subgcl  13764  issubgrpd2  13770  isnsg  13782  nmznsg  13793  isghm  13823  resghm  13840  iscmn  13873  iscmnd  13878  imasabl  13916  rngass  13945  rngcl  13950  rngpropd  13961  dfur2g  13968  issrg  13971  srgcl  13976  srgass  13977  srgideu  13978  issrgid  13987  srgpcomp  13996  srgpcompp  13997  isring  14006  ringcl  14019  crngcom  14020  iscrng2  14021  ringass  14022  ringideu  14023  isringid  14031  ringidss  14035  ringpropd  14044  ring1  14065  opprmulg  14077  oppr0g  14087  oppr1g  14088  opprnegg  14089  mulgass3  14091  dvdsrvald  14100  dvdsrd  14101  opprunitd  14117  dvrvald  14141  rdivmuldivd  14151  rhmmul  14171  isrhm2d  14172  rhmopp  14183  rhmunitinv  14185  islring  14199  lringuplu  14203  subrngmcl  14216  subrg1  14238  subrgmcl  14240  subrgdvds  14242  subrguss  14243  subrginv  14244  subrgdv  14245  subrgunit  14246  subrgugrp  14247  issubrg3  14254  rhmpropd  14261  rrgval  14269  aprval  14289  aprap  14293  islmod  14298  islmodd  14300  scaffvalg  14313  lmodpropd  14356  lsssetm  14363  islssmd  14366  islidlm  14486  lidlacl  14491  rnglidlmmgm  14503  rnglidlmsgrp  14504  rnglidlrng  14505  rspsn  14541  psrval  14673  psradd  14686  mpladd  14711  blfvalps  15102  lgseisenlem3  15794  lgseisenlem4  15795