Theorem oveqd 6105

Description: Equality deduction for operation value. (Contributed by NM, 9-Sep-2006.)

Hypothesis

Ref	Expression
oveq1d.1	|- ( ph -> A = B )

Assertion

Ref	Expression
oveqd	|- ( ph -> ( C A D ) = ( C B D ) )

Proof of Theorem oveqd

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq 6094	. 2 |- ( A = B -> ( C A D ) = ( C B D ) )
3	1, 2	syl 14	1 |- ( ph -> ( C A D ) = ( C B D ) )

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  10909  imasex  13685  imasival  13686  plusffvalg  13741  mgm1  13749  grpidvalg  13752  grpidd  13762  gzsumress  13771  sgrp1  13785  issgrpd  13786  ismndd  13809  issubmnd  13814  mnd1  13821  ismhm  13827  mhmex  13828  issubm  13838  resmhm  13853  resmhm2  13854  resmhm2b  13855  isgrp  13870  isgrpd2e  13884  grpidd2  13905  grpinvfvalg  13906  grp1  13970  imasgrp2  13972  imasgrp  13973  subg0  14042  subginv  14043  subgcl  14046  issubgrpd2  14052  isnsg  14064  nmznsg  14075  isghm  14105  resghm  14122  cntzex  14150  cntzfval  14152  resscntz  14166  iscmn  14186  iscmnd  14191  cmnsubm  14202  imasabl  14230  prdsex  14279  prdsval  14280  pwsplusgval  14315  pwsmulrval  14316  rngass  14345  rngcl  14350  rngpropd  14361  dfur2g  14373  issrg  14376  srgcl  14381  srgass  14382  srgideu  14383  issrgid  14392  srgpcomp  14401  srgpcompp  14402  isring  14411  ringcl  14424  crngcom  14425  iscrng2  14426  ringass  14427  ringideu  14428  isringid  14437  ringidss  14441  ringpropd  14450  ring1  14471  opprmulg  14485  oppr0g  14496  oppr1g  14497  opprnegg  14498  mulgass3  14500  dvdsrvald  14509  dvdsrd  14510  opprunitd  14526  dvrvald  14550  rdivmuldivd  14560  rhmmul  14580  isrhm2d  14581  rhmopp  14592  rhmunitinv  14594  islring  14608  lringuplu  14612  opprlring  14613  subrngmcl  14626  subrg1  14648  subrgmcl  14650  subrgdvds  14652  subrguss  14653  subrginv  14654  subrgdv  14655  subrgunit  14656  subrgugrp  14657  issubrg3  14664  rhmpropd  14671  rrgval  14679  aprval  14700  aprap  14707  aprprop  14710  islmod  14736  islmodd  14738  scaffvalg  14752  lmodpropd  14795  lsssetm  14802  islssmd  14805  islidlm  14925  lidlacl  14930  rnglidlmmgm  14942  rnglidlmsgrp  14943  rnglidlrng  14944  rspsn  14980  isassa  15111  isassad  15120  assamulgscmlem2  15151  psrval  15159  psradd  15183  mpladd  15220  blfvalps  15611  lgseisenlem3  16396  lgseisenlem4  16397