Theorem oveqd 5942

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

Syntax hints:   → wi 4   = wceq 1364  (class class class)co 5925

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  oveq123d  5946  oveqdr  5953  csbov12g  5965  ovmpodxf  6052  oprssov  6069  ofeqd  6141  ofeq  6142  fnmpoovd  6282  seqeq2  10560  prdsex  12971  prdsval  12975  pwsplusgval  12997  pwsmulrval  12998  imasex  13007  imasival  13008  plusffvalg  13064  mgm1  13072  grpidvalg  13075  grpidd  13085  gsumress  13097  sgrp1  13113  issgrpd  13114  ismndd  13139  issubmnd  13144  mnd1  13157  ismhm  13163  mhmex  13164  issubm  13174  resmhm  13189  resmhm2  13190  resmhm2b  13191  isgrp  13208  isgrpd2e  13222  grpidd2  13243  grpinvfvalg  13244  grp1  13308  imasgrp2  13316  imasgrp  13317  subg0  13386  subginv  13387  subgcl  13390  issubgrpd2  13396  isnsg  13408  nmznsg  13419  isghm  13449  resghm  13466  iscmn  13499  iscmnd  13504  imasabl  13542  rngass  13571  rngcl  13576  rngpropd  13587  dfur2g  13594  issrg  13597  srgcl  13602  srgass  13603  srgideu  13604  issrgid  13613  srgpcomp  13622  srgpcompp  13623  isring  13632  ringcl  13645  crngcom  13646  iscrng2  13647  ringass  13648  ringideu  13649  isringid  13657  ringidss  13661  ringpropd  13670  ring1  13691  opprmulg  13703  oppr0g  13713  oppr1g  13714  opprnegg  13715  mulgass3  13717  reldvdsrsrg  13724  dvdsrvald  13725  dvdsrd  13726  opprunitd  13742  dvrvald  13766  rdivmuldivd  13776  rhmmul  13796  isrhm2d  13797  rhmopp  13808  rhmunitinv  13810  islring  13824  lringuplu  13828  subrngmcl  13841  subrg1  13863  subrgmcl  13865  subrgdvds  13867  subrguss  13868  subrginv  13869  subrgdv  13870  subrgunit  13871  subrgugrp  13872  issubrg3  13879  rhmpropd  13886  rrgval  13894  aprval  13914  aprap  13918  islmod  13923  islmodd  13925  scaffvalg  13938  lmodpropd  13981  lsssetm  13988  islssmd  13991  islidlm  14111  lidlacl  14116  rnglidlmmgm  14128  rnglidlmsgrp  14129  rnglidlrng  14130  rspsn  14166  psrval  14296  psradd  14307  blfvalps  14705  lgseisenlem3  15397  lgseisenlem4  15398