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  10888  imasex  13626  imasival  13627  plusffvalg  13682  mgm1  13690  grpidvalg  13693  grpidd  13703  gzsumress  13712  sgrp1  13726  issgrpd  13727  ismndd  13750  issubmnd  13755  mnd1  13762  ismhm  13768  mhmex  13769  issubm  13779  resmhm  13794  resmhm2  13795  resmhm2b  13796  isgrp  13811  isgrpd2e  13825  grpidd2  13846  grpinvfvalg  13847  grp1  13911  imasgrp2  13913  imasgrp  13914  subg0  13983  subginv  13984  subgcl  13987  issubgrpd2  13993  isnsg  14005  nmznsg  14016  isghm  14046  resghm  14063  iscmn  14096  iscmnd  14101  cmnsubm  14112  imasabl  14140  prdsex  14172  prdsval  14173  pwsplusgval  14208  pwsmulrval  14209  rngass  14238  rngcl  14243  rngpropd  14254  dfur2g  14266  issrg  14269  srgcl  14274  srgass  14275  srgideu  14276  issrgid  14285  srgpcomp  14294  srgpcompp  14295  isring  14304  ringcl  14317  crngcom  14318  iscrng2  14319  ringass  14320  ringideu  14321  isringid  14330  ringidss  14334  ringpropd  14343  ring1  14364  opprmulg  14376  oppr0g  14387  oppr1g  14388  opprnegg  14389  mulgass3  14391  dvdsrvald  14400  dvdsrd  14401  opprunitd  14417  dvrvald  14441  rdivmuldivd  14451  rhmmul  14471  isrhm2d  14472  rhmopp  14483  rhmunitinv  14485  islring  14499  lringuplu  14503  opprlring  14504  subrngmcl  14517  subrg1  14539  subrgmcl  14541  subrgdvds  14543  subrguss  14544  subrginv  14545  subrgdv  14546  subrgunit  14547  subrgugrp  14548  issubrg3  14555  rhmpropd  14562  rrgval  14570  aprval  14591  aprap  14598  aprprop  14601  islmod  14627  islmodd  14629  scaffvalg  14643  lmodpropd  14686  lsssetm  14693  islssmd  14696  islidlm  14816  lidlacl  14821  rnglidlmmgm  14833  rnglidlmsgrp  14834  rnglidlrng  14835  rspsn  14871  isassa  15002  isassad  15011  assamulgscmlem2  15042  psrval  15050  psradd  15070  mpladd  15095  blfvalps  15486  lgseisenlem3  16191  lgseisenlem4  16192