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  10903  imasex  13679  imasival  13680  plusffvalg  13735  mgm1  13743  grpidvalg  13746  grpidd  13756  gzsumress  13765  sgrp1  13779  issgrpd  13780  ismndd  13803  issubmnd  13808  mnd1  13815  ismhm  13821  mhmex  13822  issubm  13832  resmhm  13847  resmhm2  13848  resmhm2b  13849  isgrp  13864  isgrpd2e  13878  grpidd2  13899  grpinvfvalg  13900  grp1  13964  imasgrp2  13966  imasgrp  13967  subg0  14036  subginv  14037  subgcl  14040  issubgrpd2  14046  isnsg  14058  nmznsg  14069  isghm  14099  resghm  14116  cntzex  14144  cntzfval  14146  resscntz  14160  iscmn  14180  iscmnd  14185  cmnsubm  14196  imasabl  14224  prdsex  14256  prdsval  14257  pwsplusgval  14292  pwsmulrval  14293  rngass  14322  rngcl  14327  rngpropd  14338  dfur2g  14350  issrg  14353  srgcl  14358  srgass  14359  srgideu  14360  issrgid  14369  srgpcomp  14378  srgpcompp  14379  isring  14388  ringcl  14401  crngcom  14402  iscrng2  14403  ringass  14404  ringideu  14405  isringid  14414  ringidss  14418  ringpropd  14427  ring1  14448  opprmulg  14460  oppr0g  14471  oppr1g  14472  opprnegg  14473  mulgass3  14475  dvdsrvald  14484  dvdsrd  14485  opprunitd  14501  dvrvald  14525  rdivmuldivd  14535  rhmmul  14555  isrhm2d  14556  rhmopp  14567  rhmunitinv  14569  islring  14583  lringuplu  14587  opprlring  14588  subrngmcl  14601  subrg1  14623  subrgmcl  14625  subrgdvds  14627  subrguss  14628  subrginv  14629  subrgdv  14630  subrgunit  14631  subrgugrp  14632  issubrg3  14639  rhmpropd  14646  rrgval  14654  aprval  14675  aprap  14682  aprprop  14685  islmod  14711  islmodd  14713  scaffvalg  14727  lmodpropd  14770  lsssetm  14777  islssmd  14780  islidlm  14900  lidlacl  14905  rnglidlmmgm  14917  rnglidlmsgrp  14918  rnglidlrng  14919  rspsn  14955  isassa  15086  isassad  15095  assamulgscmlem2  15126  psrval  15134  psradd  15155  mpladd  15186  blfvalps  15577  lgseisenlem3  16357  lgseisenlem4  16358