Theorem oveqd 5894

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

Syntax hints:   → wi 4   = wceq 1353  (class class class)co 5877

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3812  df-br 4006  df-iota 5180  df-fv 5226  df-ov 5880

This theorem is referenced by:  oveq123d  5898  oveqdr  5905  csbov12g  5916  ovmpodxf  6002  oprssov  6018  ofeq  6087  fnmpoovd  6218  seqeq2  10451  prdsex  12723  imasex  12731  imasival  12732  plusffvalg  12786  mgm1  12794  grpidvalg  12797  grpidd  12807  sgrp1  12821  ismndd  12843  issubmnd  12848  mnd1  12852  ismhm  12858  issubm  12868  isgrp  12888  isgrpd2e  12901  grpidd2  12919  grpinvfvalg  12920  grp1  12981  subg0  13045  subginv  13046  subgcl  13049  issubgrpd2  13055  isnsg  13067  nmznsg  13078  iscmn  13101  iscmnd  13106  dfur2g  13150  issrg  13153  srgcl  13158  srgass  13159  srgideu  13160  issrgid  13169  srgpcomp  13178  srgpcompp  13179  isring  13188  ringcl  13201  crngcom  13202  iscrng2  13203  ringass  13204  ringideu  13205  isringid  13213  ringidss  13217  ringpropd  13222  ring1  13241  opprmulg  13248  oppr0g  13256  oppr1g  13257  opprnegg  13258  mulgass3  13259  reldvdsrsrg  13266  dvdsrvald  13267  dvdsrd  13268  opprunitd  13284  dvrvald  13308  rdivmuldivd  13318  islring  13338  lringuplu  13342  subrg1  13357  subrgmcl  13359  subrgdvds  13361  subrguss  13362  subrginv  13363  subrgdv  13364  subrgunit  13365  subrgugrp  13366  issubrg3  13373  aprval  13377  aprap  13381  islmod  13386  islmodd  13388  scaffvalg  13401  lmodpropd  13444  lsssetm  13449  islssmd  13451  blfvalps  13970