Theorem oveqd 5892

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 5881	. 2 |- ( A = B -> ( C A D ) = ( C B D ) )
3	1, 2	syl 14	1 |- ( ph -> ( C A D ) = ( C B D ) )

Syntax hints:   -> wi 4   = wceq 1353  (class class class)co 5875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878

This theorem is referenced by:  oveq123d  5896  oveqdr  5903  csbov12g  5914  ovmpodxf  6000  oprssov  6016  ofeq  6085  fnmpoovd  6216  seqeq2  10449  prdsex  12718  imasex  12726  imasival  12727  plusffvalg  12781  mgm1  12789  grpidvalg  12792  grpidd  12802  sgrp1  12816  ismndd  12838  issubmnd  12843  mnd1  12847  ismhm  12853  issubm  12863  isgrp  12883  isgrpd2e  12896  grpidd2  12914  grpinvfvalg  12915  grp1  12976  subg0  13040  subginv  13041  subgcl  13044  issubgrpd2  13050  isnsg  13062  nmznsg  13073  iscmn  13096  iscmnd  13101  dfur2g  13145  issrg  13148  srgcl  13153  srgass  13154  srgideu  13155  issrgid  13164  srgpcomp  13173  srgpcompp  13174  isring  13183  ringcl  13196  crngcom  13197  iscrng2  13198  ringass  13199  ringideu  13200  isringid  13208  ringidss  13212  ringpropd  13217  ring1  13236  opprmulg  13243  oppr0g  13251  oppr1g  13252  opprnegg  13253  mulgass3  13254  reldvdsrsrg  13261  dvdsrvald  13262  dvdsrd  13263  opprunitd  13279  dvrvald  13303  rdivmuldivd  13313  islring  13333  lringuplu  13337  subrg1  13352  subrgmcl  13354  subrgdvds  13356  subrguss  13357  subrginv  13358  subrgdv  13359  subrgunit  13360  subrgugrp  13361  issubrg3  13368  aprval  13372  aprap  13376  islmod  13381  islmodd  13383  scaffvalg  13396  lmodpropd  13439  blfvalps  13888