Theorem oveqd 6066

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

Syntax hints:   → wi 4   = wceq 1398  (class class class)co 6049

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-uni 3914  df-br 4109  df-iota 5311  df-fv 5359  df-ov 6052

This theorem is referenced by:  oveq123d  6070  oveqdr  6077  csbov12g  6089  ovmpodxf  6178  oprssov  6195  ofeqd  6267  ofeq  6268  fnmpoovd  6410  seqeq2  10809  prdsex  13471  prdsval  13475  pwsplusgval  13497  pwsmulrval  13498  imasex  13507  imasival  13508  plusffvalg  13564  mgm1  13572  grpidvalg  13575  grpidd  13585  gsumress  13597  sgrp1  13613  issgrpd  13614  ismndd  13639  issubmnd  13644  mnd1  13657  ismhm  13663  mhmex  13664  issubm  13674  resmhm  13689  resmhm2  13690  resmhm2b  13691  isgrp  13708  isgrpd2e  13722  grpidd2  13743  grpinvfvalg  13744  grp1  13808  imasgrp2  13816  imasgrp  13817  subg0  13886  subginv  13887  subgcl  13890  issubgrpd2  13896  isnsg  13908  nmznsg  13919  isghm  13949  resghm  13966  iscmn  13999  iscmnd  14004  imasabl  14042  rngass  14072  rngcl  14077  rngpropd  14088  dfur2g  14095  issrg  14098  srgcl  14103  srgass  14104  srgideu  14105  issrgid  14114  srgpcomp  14123  srgpcompp  14124  isring  14133  ringcl  14146  crngcom  14147  iscrng2  14148  ringass  14149  ringideu  14150  isringid  14158  ringidss  14162  ringpropd  14171  ring1  14192  opprmulg  14204  oppr0g  14214  oppr1g  14215  opprnegg  14216  mulgass3  14218  dvdsrvald  14227  dvdsrd  14228  opprunitd  14244  dvrvald  14268  rdivmuldivd  14278  rhmmul  14298  isrhm2d  14299  rhmopp  14310  rhmunitinv  14312  islring  14326  lringuplu  14330  subrngmcl  14343  subrg1  14365  subrgmcl  14367  subrgdvds  14369  subrguss  14370  subrginv  14371  subrgdv  14372  subrgunit  14373  subrgugrp  14374  issubrg3  14381  rhmpropd  14388  rrgval  14396  aprval  14417  aprap  14421  islmod  14426  islmodd  14428  scaffvalg  14441  lmodpropd  14484  lsssetm  14491  islssmd  14494  islidlm  14614  lidlacl  14619  rnglidlmmgm  14631  rnglidlmsgrp  14632  rnglidlrng  14633  rspsn  14669  psrval  14801  psradd  14821  mpladd  14846  blfvalps  15237  lgseisenlem3  15932  lgseisenlem4  15933