Theorem oveqd 6105

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  (class class class)co 6088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-uni 3936  df-br 4132  df-iota 5340  df-fv 5388  df-ov 6091

This theorem is used by:  oveq123d  6109  oveqdr  6116  csbov12g  6128  ovmpodxf  6217  oprssov  6234  ofeqd  6307  ofeq  6308  fnmpoovd  6455  seqeq2  10910  imasex  13686  imasival  13687  plusffvalg  13742  mgm1  13750  grpidvalg  13753  grpidd  13763  gzsumress  13772  sgrp1  13786  issgrpd  13787  ismndd  13810  issubmnd  13815  mnd1  13822  ismhm  13828  mhmex  13829  issubm  13839  resmhm  13854  resmhm2  13855  resmhm2b  13856  isgrp  13871  isgrpd2e  13885  grpidd2  13906  grpinvfvalg  13907  grp1  13971  imasgrp2  13973  imasgrp  13974  subg0  14043  subginv  14044  subgcl  14047  issubgrpd2  14053  isnsg  14065  nmznsg  14076  isghm  14106  resghm  14123  cntzex  14151  cntzfval  14153  resscntz  14167  iscmn  14187  iscmnd  14192  cmnsubm  14203  imasabl  14231  prdsex  14280  prdsval  14281  pwsplusgval  14316  pwsmulrval  14317  rngass  14346  rngcl  14351  rngpropd  14362  dfur2g  14374  issrg  14377  srgcl  14382  srgass  14383  srgideu  14384  issrgid  14393  srgpcomp  14402  srgpcompp  14403  isring  14412  ringcl  14425  crngcom  14426  iscrng2  14427  ringass  14428  ringideu  14429  isringid  14438  ringidss  14442  ringpropd  14451  ring1  14472  opprmulg  14486  oppr0g  14497  oppr1g  14498  opprnegg  14499  mulgass3  14501  dvdsrvald  14510  dvdsrd  14511  opprunitd  14527  dvrvald  14551  rdivmuldivd  14561  rhmmul  14581  isrhm2d  14582  rhmopp  14593  rhmunitinv  14595  islring  14609  lringuplu  14613  opprlring  14614  subrngmcl  14627  subrg1  14649  subrgmcl  14651  subrgdvds  14653  subrguss  14654  subrginv  14655  subrgdv  14656  subrgunit  14657  subrgugrp  14658  issubrg3  14665  rhmpropd  14672  rrgval  14680  aprval  14701  aprap  14708  aprprop  14711  islmod  14737  islmodd  14739  scaffvalg  14753  lmodpropd  14796  lsssetm  14803  islssmd  14806  islidlm  14926  lidlacl  14931  rnglidlmmgm  14943  rnglidlmsgrp  14944  rnglidlrng  14945  rspsn  14981  isassa  15112  isassad  15121  assamulgscmlem2  15152  psrval  15162  psradd  15188  mpladd  15232  blfvalps  15623  lgseisenlem3  16408  lgseisenlem4  16409