Theorem oveq2d 5548

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

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveq2d	⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Proof of Theorem oveq2d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq2 5540	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1284  (class class class)co 5532

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-3an 921  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-rex 2354  df-v 2603  df-un 2977  df-sn 3404  df-pr 3405  df-op 3407  df-uni 3602  df-br 3786  df-iota 4887  df-fv 4930  df-ov 5535

This theorem is referenced by:  csbov1g  5565  caovassg  5679  caovdig  5695  caovdirg  5698  caov32d  5701  caov4d  5705  caov42d  5707  grprinvlem  5715  grprinvd  5716  grpridd  5717  nnaass  6087  nndi  6088  nnmass  6089  nnmsucr  6090  ecovass  6238  ecoviass  6239  ecovdi  6240  ecovidi  6241  addasspig  6520  mulasspig  6522  distrpig  6523  dfplpq2  6544  mulpipq2  6561  addassnqg  6572  prarloclemarch  6608  prarloclemarch2  6609  ltrnqg  6610  enq0sym  6622  addnq0mo  6637  mulnq0mo  6638  addnnnq0  6639  nq0a0  6647  distrnq0  6649  addassnq0  6652  prarloclemlo  6684  prarloclem3  6687  prarloclem5  6690  prarloclemcalc  6692  addnqprl  6719  addnqpru  6720  prmuloclemcalc  6755  mulnqprl  6758  mulnqpru  6759  distrlem4prl  6774  distrlem4pru  6775  1idprl  6780  1idpru  6781  ltexprlemloc  6797  addcanprleml  6804  addcanprlemu  6805  recexprlem1ssu  6824  ltmprr  6832  caucvgprlemcanl  6834  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  cauappcvgprlem1  6849  cauappcvgprlemlim  6851  caucvgprlemnkj  6856  caucvgprlemnbj  6857  caucvgprlemdisj  6864  caucvgprlemloc  6865  caucvgprlemcl  6866  caucvgprlemladdrl  6868  caucvgprlem1  6869  caucvgpr  6872  caucvgprprlemell  6875  caucvgprprlemcbv  6877  caucvgprprlemval  6878  caucvgprprlemnkeqj  6880  caucvgprprlemopl  6887  caucvgprprlemlol  6888  caucvgprprlemloc  6893  caucvgprprlemclphr  6895  caucvgprprlemexb  6897  caucvgprprlemaddq  6898  caucvgprprlem1  6899  addcmpblnr  6916  mulcmpblnrlemg  6917  addsrmo  6920  mulsrmo  6921  addsrpr  6922  mulsrpr  6923  ltsrprg  6924  recexgt0sr  6950  mulgt0sr  6954  caucvgsrlemgt1  6971  caucvgsrlemoffval  6972  caucvgsr  6978  mulcnsr  7003  pitoregt0  7017  recidpirqlemcalc  7025  axmulcom  7037  axmulass  7039  axdistr  7040  ax0id  7044  axcnre  7047  recriota  7056  axcaucvglemcau  7064  axcaucvglemres  7065  mulid1  7116  adddirp1d  7145  mul32  7238  mul31  7239  add32  7267  add4  7269  add42  7270  cnegex  7286  addcan2  7289  addsubass  7318  subsub2  7336  nppcan2  7339  sub32  7342  nnncan  7343  sub4  7353  muladd  7488  subdi  7489  mul2neg  7502  submul2  7503  mulsub  7505  mulsubfacd  7522  add20  7578  recexre  7678  rereim  7686  apreap  7687  ltmul1  7692  cru  7702  apreim  7703  mulreim  7704  apadd1  7708  apneg  7711  mulap0  7744  divrecap  7776  divassap  7778  divmulasscomap  7784  divsubdirap  7796  divdivdivap  7801  divmul24ap  7804  divmuleqap  7805  divcanap6  7807  divdivap1  7811  divdivap2  7812  divsubdivap  7816  conjmulap  7817  div2negap  7823  apmul1  7876  cju  8038  nnmulcl  8060  add1p1  8280  sub1m1  8281  cnm2m1cnm3  8282  xp1d2m1eqxm1d2  8283  div4p1lem1div2  8284  un0addcl  8321  un0mulcl  8322  zaddcllemneg  8390  qapne  8724  cnref1o  8733  lincmb01cmp  9025  iccf1o  9026  ige3m2fz  9068  fztp  9095  fzsuc2  9096  fseq1m1p1  9112  fzm1  9117  ige2m1fz1  9126  nn0split  9147  fzval3  9213  zpnn0elfzo1  9217  fzosplitsnm1  9218  fzosplitprm1  9243  fzoshftral  9247  rebtwn2zlemstep  9261  flhalf  9304  modqval  9326  modqvalr  9327  modqdiffl  9337  modqfrac  9339  flqmod  9340  intqfrac  9341  zmod10  9342  modqmulnn  9344  modqvalp1  9345  modqid  9351  modqcyc  9361  modqcyc2  9362  modqmul1  9379  q2submod  9387  modqdi  9394  modqsubdir  9395  modqeqmodmin  9396  modsumfzodifsn  9398  addmodlteq  9400  uzsinds  9428  iseqeq3  9436  iseqval  9440  iseqp1  9445  iseqm1  9447  iseqfveq2  9448  iseqshft2  9452  monoord2  9456  isermono  9457  iseqsplit  9458  iseqcaopr3  9460  iseqcaopr2  9461  iseqcaopr  9462  iseqhomo  9468  iseqz  9469  expivallem  9477  expival  9478  expp1  9483  expnegap0  9484  expineg2  9485  expn1ap0  9486  expm1t  9504  1exp  9505  expnegzap  9510  mulexpzap  9516  expadd  9518  expaddzaplem  9519  expaddzap  9520  expmul  9521  expmulzap  9522  m1expeven  9523  expsubap  9524  expp1zap  9525  expm1ap  9526  expdivap  9527  iexpcyc  9579  subsq2  9582  binom2  9585  binom21  9586  binom2sub  9587  mulbinom2  9589  binom3  9590  zesq  9591  bernneq  9593  sqoddm1div8  9625  nn0opthlem1d  9647  nn0opthd  9649  facp1  9657  facnn2  9661  faclbnd  9668  faclbnd6  9671  bcval  9676  bccmpl  9681  bcn0  9682  bcnn  9684  bcnp1n  9686  bcm1k  9687  bcp1n  9688  bcp1nk  9689  ibcval5  9690  bcp1m1  9692  bcpasc  9693  bcn2m1  9696  bcn2p1  9697  shftcan1  9722  shftcan2  9723  cjval  9732  cjth  9733  crre  9744  replim  9746  remim  9747  reim0b  9749  rereb  9750  mulreap  9751  cjreb  9753  recj  9754  reneg  9755  readd  9756  resub  9757  remullem  9758  imcj  9762  imneg  9763  imadd  9764  imsub  9765  cjcj  9770  cjadd  9771  ipcnval  9773  cjmulrcl  9774  cjneg  9777  addcj  9778  cjsub  9779  cnrecnv  9797  caucvgrelemcau  9866  cvg1nlemcau  9870  cvg1nlemres  9871  recvguniqlem  9880  resqrexlemover  9896  resqrexlemlo  9899  resqrexlemcalc1  9900  resqrexlemcalc3  9902  resqrexlemnm  9904  resqrexlemcvg  9905  absneg  9936  abscj  9938  sqabsadd  9941  sqabssub  9942  absmul  9955  absid  9957  absre  9963  absresq  9964  absexpzap  9966  recvalap  9983  abstri  9990  abs2dif2  9993  recan  9995  cau3lem  10000  amgm2  10004  climaddc1  10167  climsubc1  10170  climcvg1nlem  10186  serif0  10189  dvdsexp  10261  oexpneg  10276  opeo  10297  omeo  10298  m1exp1  10301  flodddiv4  10334  flodddiv4t2lthalf  10337  divgcdnnr  10367  gcdaddm  10375  gcdadd  10376  gcdid  10377  modgcd  10382  bezoutlemnewy  10385  bezoutlema  10388  bezoutlemb  10389  bezoutlemex  10390  bezoutlembz  10393  absmulgcd  10406  gcdmultiple  10409  gcdmultiplez  10410  rpmulgcd  10415  rplpwr  10416  eucalginv  10438  eucialg  10441  lcmneg  10456  lcmgcdlem  10459  lcmgcd  10460  lcmid  10462  lcm1  10463  mulgcddvds  10476  qredeq  10478  divgcdcoprmex  10484  prmind2  10502  rpexp1i  10533  pw2dvdslemn  10543  pw2dvdseulemle  10545  pw2dvdseu  10546  oddpwdclemxy  10547  oddpwdclemdvds  10548  oddpwdclemndvds  10549  oddpwdclemdc  10551  2sqpwodd  10554  qdencn  10785