Theorem oveqd 5961

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

Syntax hints:   → wi 4   = wceq 1373  (class class class)co 5944

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279  df-ov 5947

This theorem is referenced by:  oveq123d  5965  oveqdr  5972  csbov12g  5984  ovmpodxf  6071  oprssov  6088  ofeqd  6160  ofeq  6161  fnmpoovd  6301  seqeq2  10596  prdsex  13101  prdsval  13105  pwsplusgval  13127  pwsmulrval  13128  imasex  13137  imasival  13138  plusffvalg  13194  mgm1  13202  grpidvalg  13205  grpidd  13215  gsumress  13227  sgrp1  13243  issgrpd  13244  ismndd  13269  issubmnd  13274  mnd1  13287  ismhm  13293  mhmex  13294  issubm  13304  resmhm  13319  resmhm2  13320  resmhm2b  13321  isgrp  13338  isgrpd2e  13352  grpidd2  13373  grpinvfvalg  13374  grp1  13438  imasgrp2  13446  imasgrp  13447  subg0  13516  subginv  13517  subgcl  13520  issubgrpd2  13526  isnsg  13538  nmznsg  13549  isghm  13579  resghm  13596  iscmn  13629  iscmnd  13634  imasabl  13672  rngass  13701  rngcl  13706  rngpropd  13717  dfur2g  13724  issrg  13727  srgcl  13732  srgass  13733  srgideu  13734  issrgid  13743  srgpcomp  13752  srgpcompp  13753  isring  13762  ringcl  13775  crngcom  13776  iscrng2  13777  ringass  13778  ringideu  13779  isringid  13787  ringidss  13791  ringpropd  13800  ring1  13821  opprmulg  13833  oppr0g  13843  oppr1g  13844  opprnegg  13845  mulgass3  13847  reldvdsrsrg  13854  dvdsrvald  13855  dvdsrd  13856  opprunitd  13872  dvrvald  13896  rdivmuldivd  13906  rhmmul  13926  isrhm2d  13927  rhmopp  13938  rhmunitinv  13940  islring  13954  lringuplu  13958  subrngmcl  13971  subrg1  13993  subrgmcl  13995  subrgdvds  13997  subrguss  13998  subrginv  13999  subrgdv  14000  subrgunit  14001  subrgugrp  14002  issubrg3  14009  rhmpropd  14016  rrgval  14024  aprval  14044  aprap  14048  islmod  14053  islmodd  14055  scaffvalg  14068  lmodpropd  14111  lsssetm  14118  islssmd  14121  islidlm  14241  lidlacl  14246  rnglidlmmgm  14258  rnglidlmsgrp  14259  rnglidlrng  14260  rspsn  14296  psrval  14428  psradd  14441  mpladd  14466  blfvalps  14857  lgseisenlem3  15549  lgseisenlem4  15550