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  10562  prdsex  12973  prdsval  12977  pwsplusgval  12999  pwsmulrval  13000  imasex  13009  imasival  13010  plusffvalg  13066  mgm1  13074  grpidvalg  13077  grpidd  13087  gsumress  13099  sgrp1  13115  issgrpd  13116  ismndd  13141  issubmnd  13146  mnd1  13159  ismhm  13165  mhmex  13166  issubm  13176  resmhm  13191  resmhm2  13192  resmhm2b  13193  isgrp  13210  isgrpd2e  13224  grpidd2  13245  grpinvfvalg  13246  grp1  13310  imasgrp2  13318  imasgrp  13319  subg0  13388  subginv  13389  subgcl  13392  issubgrpd2  13398  isnsg  13410  nmznsg  13421  isghm  13451  resghm  13468  iscmn  13501  iscmnd  13506  imasabl  13544  rngass  13573  rngcl  13578  rngpropd  13589  dfur2g  13596  issrg  13599  srgcl  13604  srgass  13605  srgideu  13606  issrgid  13615  srgpcomp  13624  srgpcompp  13625  isring  13634  ringcl  13647  crngcom  13648  iscrng2  13649  ringass  13650  ringideu  13651  isringid  13659  ringidss  13663  ringpropd  13672  ring1  13693  opprmulg  13705  oppr0g  13715  oppr1g  13716  opprnegg  13717  mulgass3  13719  reldvdsrsrg  13726  dvdsrvald  13727  dvdsrd  13728  opprunitd  13744  dvrvald  13768  rdivmuldivd  13778  rhmmul  13798  isrhm2d  13799  rhmopp  13810  rhmunitinv  13812  islring  13826  lringuplu  13830  subrngmcl  13843  subrg1  13865  subrgmcl  13867  subrgdvds  13869  subrguss  13870  subrginv  13871  subrgdv  13872  subrgunit  13873  subrgugrp  13874  issubrg3  13881  rhmpropd  13888  rrgval  13896  aprval  13916  aprap  13920  islmod  13925  islmodd  13927  scaffvalg  13940  lmodpropd  13983  lsssetm  13990  islssmd  13993  islidlm  14113  lidlacl  14118  rnglidlmmgm  14130  rnglidlmsgrp  14131  rnglidlrng  14132  rspsn  14168  psrval  14300  psradd  14313  mpladd  14338  blfvalps  14729  lgseisenlem3  15421  lgseisenlem4  15422