Theorem oveqd 5891

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

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

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 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877

This theorem is referenced by:  oveq123d  5895  oveqdr  5902  csbov12g  5913  ovmpodxf  5999  oprssov  6015  ofeq  6084  fnmpoovd  6215  seqeq2  10446  imasex  12708  imasival  12709  plusffvalg  12735  mgm1  12743  grpidvalg  12746  grpidd  12756  sgrp1  12770  ismndd  12792  issubmnd  12797  mnd1  12801  ismhm  12807  issubm  12817  isgrp  12837  isgrpd2e  12850  grpidd2  12868  grpinvfvalg  12869  grp1  12930  subg0  12993  subginv  12994  subgcl  12997  issubgrpd2  13003  isnsg  13015  nmznsg  13026  iscmn  13049  iscmnd  13054  dfur2g  13098  issrg  13101  srgcl  13106  srgass  13107  srgideu  13108  issrgid  13117  srgpcomp  13126  srgpcompp  13127  isring  13136  ringcl  13149  crngcom  13150  iscrng2  13151  ringass  13152  ringideu  13153  isringid  13161  ringidss  13165  ringpropd  13170  ring1  13189  opprmulg  13196  oppr0g  13204  oppr1g  13205  opprnegg  13206  mulgass3  13207  reldvdsrsrg  13214  dvdsrvald  13215  dvdsrd  13216  opprunitd  13232  dvrvald  13256  rdivmuldivd  13266  islring  13286  lringuplu  13290  aprval  13293  aprap  13297  subrg1  13312  subrgmcl  13314  subrgdvds  13316  subrguss  13317  subrginv  13318  subrgdv  13319  subrgunit  13320  subrgugrp  13321  issubrg3  13328  blfvalps  13778