Theorem oveqd 6102

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 6091	. 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 6085

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 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  oveq123d  6106  oveqdr  6113  csbov12g  6125  ovmpodxf  6214  oprssov  6231  ofeqd  6304  ofeq  6305  fnmpoovd  6451  seqeq2  10901  imasex  13675  imasival  13676  plusffvalg  13731  mgm1  13739  grpidvalg  13742  grpidd  13752  gzsumress  13761  sgrp1  13775  issgrpd  13776  ismndd  13799  issubmnd  13804  mnd1  13811  ismhm  13817  mhmex  13818  issubm  13828  resmhm  13843  resmhm2  13844  resmhm2b  13845  isgrp  13860  isgrpd2e  13874  grpidd2  13895  grpinvfvalg  13896  grp1  13960  imasgrp2  13962  imasgrp  13963  subg0  14032  subginv  14033  subgcl  14036  issubgrpd2  14042  isnsg  14054  nmznsg  14065  isghm  14095  resghm  14112  iscmn  14145  iscmnd  14150  cmnsubm  14161  imasabl  14189  prdsex  14221  prdsval  14222  pwsplusgval  14257  pwsmulrval  14258  rngass  14287  rngcl  14292  rngpropd  14303  dfur2g  14315  issrg  14318  srgcl  14323  srgass  14324  srgideu  14325  issrgid  14334  srgpcomp  14343  srgpcompp  14344  isring  14353  ringcl  14366  crngcom  14367  iscrng2  14368  ringass  14369  ringideu  14370  isringid  14379  ringidss  14383  ringpropd  14392  ring1  14413  opprmulg  14425  oppr0g  14436  oppr1g  14437  opprnegg  14438  mulgass3  14440  dvdsrvald  14449  dvdsrd  14450  opprunitd  14466  dvrvald  14490  rdivmuldivd  14500  rhmmul  14520  isrhm2d  14521  rhmopp  14532  rhmunitinv  14534  islring  14548  lringuplu  14552  opprlring  14553  subrngmcl  14566  subrg1  14588  subrgmcl  14590  subrgdvds  14592  subrguss  14593  subrginv  14594  subrgdv  14595  subrgunit  14596  subrgugrp  14597  issubrg3  14604  rhmpropd  14611  rrgval  14619  aprval  14640  aprap  14647  aprprop  14650  islmod  14676  islmodd  14678  scaffvalg  14692  lmodpropd  14735  lsssetm  14742  islssmd  14745  islidlm  14865  lidlacl  14870  rnglidlmmgm  14882  rnglidlmsgrp  14883  rnglidlrng  14884  rspsn  14920  isassa  15051  isassad  15060  assamulgscmlem2  15091  psrval  15099  psradd  15119  mpladd  15144  blfvalps  15535  lgseisenlem3  16289  lgseisenlem4  16290