Theorem oveq2d 5528

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)

Hypothesis

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

Assertion

Ref	Expression
oveq2d	|- ( ph -> ( C F A ) = ( C F B ) )

Proof of Theorem oveq2d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 |- ( ph -> A = B )
2		oveq2 5520	. 2 |- ( A = B -> ( C F A ) = ( C F B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C F A ) = ( C F B ) )

Syntax hints:   -> wi 4   = wceq 1243  (class class class)co 5512

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022

This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-rex 2312  df-v 2559  df-un 2922  df-sn 3381  df-pr 3382  df-op 3384  df-uni 3581  df-br 3765  df-iota 4867  df-fv 4910  df-ov 5515

This theorem is referenced by:  csbov1g  5545  caovassg  5659  caovdig  5675  caovdirg  5678  caov32d  5681  caov4d  5685  caov42d  5687  grprinvlem  5695  grprinvd  5696  grpridd  5697  nnaass  6064  nndi  6065  nnmass  6066  nnmsucr  6067  ecovass  6215  ecoviass  6216  ecovdi  6217  ecovidi  6218  addasspig  6428  mulasspig  6430  distrpig  6431  dfplpq2  6452  mulpipq2  6469  addassnqg  6480  prarloclemarch  6516  prarloclemarch2  6517  ltrnqg  6518  enq0sym  6530  addnq0mo  6545  mulnq0mo  6546  addnnnq0  6547  nq0a0  6555  distrnq0  6557  addassnq0  6560  prarloclemlo  6592  prarloclem3  6595  prarloclem5  6598  prarloclemcalc  6600  addnqprl  6627  addnqpru  6628  prmuloclemcalc  6663  mulnqprl  6666  mulnqpru  6667  distrlem4prl  6682  distrlem4pru  6683  1idprl  6688  1idpru  6689  ltexprlemloc  6705  addcanprleml  6712  addcanprlemu  6713  recexprlem1ssu  6732  ltmprr  6740  caucvgprlemcanl  6742  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  cauappcvgprlem1  6757  cauappcvgprlemlim  6759  caucvgprlemnkj  6764  caucvgprlemnbj  6765  caucvgprlemdisj  6772  caucvgprlemloc  6773  caucvgprlemcl  6774  caucvgprlemladdrl  6776  caucvgprlem1  6777  caucvgpr  6780  caucvgprprlemell  6783  caucvgprprlemcbv  6785  caucvgprprlemval  6786  caucvgprprlemnkeqj  6788  caucvgprprlemopl  6795  caucvgprprlemlol  6796  caucvgprprlemloc  6801  caucvgprprlemclphr  6803  caucvgprprlemexb  6805  caucvgprprlemaddq  6806  caucvgprprlem1  6807  addcmpblnr  6824  mulcmpblnrlemg  6825  addsrmo  6828  mulsrmo  6829  addsrpr  6830  mulsrpr  6831  ltsrprg  6832  recexgt0sr  6858  mulgt0sr  6862  caucvgsrlemgt1  6879  caucvgsrlemoffval  6880  caucvgsr  6886  mulcnsr  6911  pitoregt0  6925  recidpirqlemcalc  6933  axmulcom  6945  axmulass  6947  axdistr  6948  ax0id  6952  axcnre  6955  recriota  6964  axcaucvglemcau  6972  axcaucvglemres  6973  mulid1  7024  mul32  7143  mul31  7144  add32  7170  add4  7172  add42  7173  cnegex  7189  addcan2  7192  addsubass  7221  subsub2  7239  nppcan2  7242  sub32  7245  nnncan  7246  sub4  7256  muladd  7381  subdi  7382  mul2neg  7395  submul2  7396  mulsub  7398  mulsubfacd  7415  add20  7469  recexre  7569  rereim  7577  apreap  7578  ltmul1  7583  cru  7593  apreim  7594  mulreim  7595  apadd1  7599  apneg  7602  mulap0  7635  divrecap  7667  divassap  7669  divsubdirap  7684  divdivdivap  7689  divmul24ap  7692  divmuleqap  7693  divcanap6  7695  divdivap1  7699  divdivap2  7700  divsubdivap  7704  conjmulap  7705  div2negap  7711  apmul1  7764  cju  7913  nnmulcl  7935  add1p1  8174  sub1m1  8175  cnm2m1cnm3  8176  div4p1lem1div2  8177  un0addcl  8215  un0mulcl  8216  zaddcllemneg  8284  qapne  8574  cnref1o  8582  lincmb01cmp  8871  iccf1o  8872  ige3m2fz  8913  fztp  8940  fzsuc2  8941  fseq1m1p1  8957  fzm1  8962  ige2m1fz1  8971  nn0split  8994  fzval3  9060  zpnn0elfzo1  9064  fzosplitsnm1  9065  fzosplitprm1  9090  fzoshftral  9094  rebtwn2zlemstep  9107  flhalf  9144  modqval  9166  modqvalr  9167  modqdiffl  9177  modqfrac  9179  flqmod  9180  intqfrac  9181  zmod10  9182  modqmulnn  9184  iseqeq3  9216  iseqval  9220  iseqp1  9225  iseqm1  9227  iseqfveq2  9228  iseqshft2  9232  monoord2  9236  isermono  9237  iseqsplit  9238  iseqcaopr3  9240  iseqcaopr2  9241  iseqcaopr  9242  iseqhomo  9248  expivallem  9256  expival  9257  expp1  9262  expnegap0  9263  expineg2  9264  expn1ap0  9265  expm1t  9283  1exp  9284  expnegzap  9289  mulexpzap  9295  expadd  9297  expaddzaplem  9298  expaddzap  9299  expmul  9300  expmulzap  9301  expsubap  9302  expp1zap  9303  expm1ap  9304  expdivap  9305  subsq2  9359  binom2  9362  binom21  9363  binom2sub  9364  binom3  9366  zesq  9367  bernneq  9369  shftcan1  9435  shftcan2  9436  cjval  9445  cjth  9446  crre  9457  replim  9459  remim  9460  reim0b  9462  rereb  9463  mulreap  9464  cjreb  9466  recj  9467  reneg  9468  readd  9469  resub  9470  remullem  9471  imcj  9475  imneg  9476  imadd  9477  imsub  9478  cjcj  9483  cjadd  9484  ipcnval  9486  cjmulrcl  9487  cjneg  9490  addcj  9491  cjsub  9492  cnrecnv  9510  caucvgrelemcau  9579  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniqlem  9592  resqrexlemover  9608  resqrexlemlo  9611  resqrexlemcalc1  9612  resqrexlemcalc3  9614  resqrexlemnm  9616  resqrexlemcvg  9617  absneg  9648  abscj  9650  sqabsadd  9653  sqabssub  9654  absmul  9667  absid  9669  absre  9673  absresq  9674  absexpzap  9676  recvalap  9693  abstri  9700  abs2dif2  9703  recan  9705  cau3lem  9710  amgm2  9714  climaddc1  9849  climsubc1  9852  climcvg1nlem  9868  serif0  9871  qdencn  10124