Theorem oveq2d 5886

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 5878	. 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 1353  (class class class)co 5870

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-3an 980  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-v 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3809  df-br 4002  df-iota 5175  df-fv 5221  df-ov 5873

This theorem is referenced by:  csbov1g  5910  caovassg  6028  caovdig  6044  caovdirg  6047  caov32d  6050  caov4d  6054  caov42d  6056  nnaass  6481  nndi  6482  nnmass  6483  nnmsucr  6484  ecovass  6639  ecoviass  6640  ecovdi  6641  ecovidi  6642  addasspig  7324  mulasspig  7326  distrpig  7327  dfplpq2  7348  mulpipq2  7365  addassnqg  7376  prarloclemarch  7412  prarloclemarch2  7413  ltrnqg  7414  enq0sym  7426  addnq0mo  7441  mulnq0mo  7442  addnnnq0  7443  nq0a0  7451  distrnq0  7453  addassnq0  7456  prarloclemlo  7488  prarloclem3  7491  prarloclem5  7494  prarloclemcalc  7496  addnqprl  7523  addnqpru  7524  prmuloclemcalc  7559  mulnqprl  7562  mulnqpru  7563  distrlem4prl  7578  distrlem4pru  7579  1idprl  7584  1idpru  7585  ltexprlemloc  7601  addcanprleml  7608  addcanprlemu  7609  recexprlem1ssu  7628  ltmprr  7636  caucvgprlemcanl  7638  cauappcvgprlemladdru  7650  cauappcvgprlemladdrl  7651  cauappcvgprlem1  7653  cauappcvgprlemlim  7655  caucvgprlemnkj  7660  caucvgprlemnbj  7661  caucvgprlemdisj  7668  caucvgprlemloc  7669  caucvgprlemcl  7670  caucvgprlemladdrl  7672  caucvgprlem1  7673  caucvgpr  7676  caucvgprprlemell  7679  caucvgprprlemcbv  7681  caucvgprprlemval  7682  caucvgprprlemnkeqj  7684  caucvgprprlemopl  7691  caucvgprprlemlol  7692  caucvgprprlemloc  7697  caucvgprprlemclphr  7699  caucvgprprlemexb  7701  caucvgprprlemaddq  7702  caucvgprprlem1  7703  addcmpblnr  7733  mulcmpblnrlemg  7734  addsrmo  7737  mulsrmo  7738  addsrpr  7739  mulsrpr  7740  ltsrprg  7741  recexgt0sr  7767  mulgt0sr  7772  caucvgsrlemgt1  7789  caucvgsrlemoffval  7790  caucvgsr  7796  suplocsrlemb  7800  suplocsrlempr  7801  suplocsrlem  7802  suplocsr  7803  mulcnsr  7829  pitoregt0  7843  recidpirqlemcalc  7851  axmulcom  7865  axmulass  7867  axdistr  7868  ax0id  7872  axcnre  7875  recriota  7884  axcaucvglemcau  7892  axcaucvglemres  7893  mulrid  7949  adddirp1d  7978  mul32  8081  mul31  8082  add32  8110  add4  8112  add42  8113  cnegex  8129  addcan2  8132  addsubass  8161  subsub2  8179  nppcan2  8182  sub32  8185  nnncan  8186  sub4  8196  muladd  8335  subdi  8336  mul2neg  8349  submul2  8350  mulsub  8352  mulsubfacd  8369  add20  8425  recexre  8529  rereim  8537  apreap  8538  ltmul1  8543  cru  8553  apreim  8554  mulreim  8555  apadd1  8559  apneg  8562  mulap0  8605  divrecap  8639  divassap  8641  divmulasscomap  8647  divsubdirap  8659  divdivdivap  8664  divmul24ap  8667  divmuleqap  8668  divcanap6  8670  divdivap1  8674  divdivap2  8675  divsubdivap  8679  conjmulap  8680  div2negap  8686  apmul1  8739  cju  8912  nnmulcl  8934  add1p1  9162  sub1m1  9163  cnm2m1cnm3  9164  xp1d2m1eqxm1d2  9165  div4p1lem1div2  9166  un0addcl  9203  un0mulcl  9204  zaddcllemneg  9286  qapne  9633  cnref1o  9644  rexsub  9847  xnegid  9853  xaddcom  9855  xnegdi  9862  xaddass  9863  xaddass2  9864  xpncan  9865  xnpcan  9866  xleadd1a  9867  xsubge0  9875  xposdif  9876  xlesubadd  9877  xadd4d  9879  lincmb01cmp  9997  iccf1o  9998  ige3m2fz  10042  fztp  10071  fzsuc2  10072  fseq1m1p1  10088  fzm1  10093  ige2m1fz1  10102  nn0split  10129  nnsplit  10130  fzval3  10197  zpnn0elfzo1  10201  fzosplitsnm1  10202  fzosplitprm1  10227  fzoshftral  10231  rebtwn2zlemstep  10246  flhalf  10295  modqval  10317  modqvalr  10318  modqdiffl  10328  modqfrac  10330  flqmod  10331  intqfrac  10332  zmod10  10333  modqmulnn  10335  modqvalp1  10336  modqid  10342  modqcyc  10352  modqcyc2  10353  modqmul1  10370  q2submod  10378  modqdi  10385  modqsubdir  10386  modqeqmodmin  10387  modsumfzodifsn  10389  addmodlteq  10391  frecuzrdgsuctlem  10416  uzsinds  10435  seqeq3  10443  iseqvalcbv  10450  seq3val  10451  seqvalcd  10452  seqf  10454  seq3p1  10455  seqovcd  10456  seqp1cd  10459  seq3m1  10461  seq3fveq2  10462  seq3shft2  10466  monoord2  10470  ser3mono  10471  seq3split  10472  seq3caopr3  10474  seq3caopr2  10475  seq3caopr  10476  seq3id2  10502  seq3homo  10503  seq3z  10504  exp3vallem  10514  exp3val  10515  expp1  10520  expnegap0  10521  expineg2  10522  expn1ap0  10523  expm1t  10541  1exp  10542  expnegzap  10547  mulexpzap  10553  expadd  10555  expaddzaplem  10556  expaddzap  10557  expmul  10558  expmulzap  10559  m1expeven  10560  expsubap  10561  expp1zap  10562  expm1ap  10563  expdivap  10564  iexpcyc  10617  subsq2  10620  binom2  10624  binom21  10625  binom2sub  10626  binom2sub1  10627  mulbinom2  10629  binom3  10630  zesq  10631  bernneq  10633  sqoddm1div8  10666  nn0opthlem1d  10691  nn0opthd  10693  facp1  10701  facnn2  10705  faclbnd  10712  faclbnd6  10715  bcval  10720  bccmpl  10725  bcn0  10726  bcnn  10728  bcnp1n  10730  bcm1k  10731  bcp1n  10732  bcp1nk  10733  bcval5  10734  bcp1m1  10736  bcpasc  10737  bcn2m1  10740  bcn2p1  10741  omgadd  10773  hashunlem  10775  hashunsng  10778  hashdifsn  10790  hashxp  10797  zfz1isolemsplit  10809  zfz1isolem1  10811  zfz1iso  10812  seq3coll  10813  shftcan1  10834  shftcan2  10835  cjval  10845  cjth  10846  crre  10857  replim  10859  remim  10860  reim0b  10862  rereb  10863  mulreap  10864  cjreb  10866  recj  10867  reneg  10868  readd  10869  resub  10870  remullem  10871  imcj  10875  imneg  10876  imadd  10877  imsub  10878  cjcj  10883  cjadd  10884  ipcnval  10886  cjmulrcl  10887  cjneg  10890  addcj  10891  cjsub  10892  cnrecnv  10910  caucvgrelemcau  10980  cvg1nlemcau  10984  cvg1nlemres  10985  recvguniqlem  10994  resqrexlemover  11010  resqrexlemlo  11013  resqrexlemcalc1  11014  resqrexlemcalc3  11016  resqrexlemnm  11018  resqrexlemcvg  11019  absneg  11050  abscj  11052  sqabsadd  11055  sqabssub  11056  absmul  11069  absid  11071  absre  11077  absresq  11078  absexpzap  11080  recvalap  11097  abstri  11104  abs2dif2  11107  recan  11109  cau3lem  11114  amgm2  11118  bdtrilem  11238  xrmaxadd  11260  xrbdtri  11275  climaddc1  11328  climsubc1  11331  climcvg1nlem  11348  serf0  11351  summodclem3  11379  summodclem2a  11380  summodc  11382  fsumsplitsn  11409  fsumm1  11415  fsumsplitsnun  11418  fsump1  11419  isummulc2  11425  fsumrev  11442  fisum0diag2  11446  fsummulc2  11447  fsumsub  11451  fsumabs  11464  telfsumo  11465  fsumparts  11469  fsumrelem  11470  fsumiun  11476  binomlem  11482  binom  11483  binom1p  11484  binom11  11485  binom1dif  11486  bcxmas  11488  isumsplit  11490  isum1p  11491  divcnv  11496  arisum2  11498  trireciplem  11499  trirecip  11500  geolim  11510  georeclim  11512  geo2sum  11513  geo2lim  11515  geoisum1c  11519  0.999...  11520  cvgratnnlemnexp  11523  cvgratnnlemmn  11524  cvgratz  11531  mertenslem2  11535  mertensabs  11536  clim2prod  11538  prodfrecap  11545  prodfdivap  11546  prodmodclem3  11574  prodmodclem2a  11575  fprodm1  11597  fprodp1  11599  fprodunsn  11603  fprodfac  11614  fprodeq0  11616  fprodconst  11619  fprodrec  11628  fproddivap  11629  fprodsplitsn  11632  ege2le3  11670  efaddlem  11673  efsub  11680  efexp  11681  eftlub  11689  efsep  11690  effsumlt  11691  ef4p  11693  tanval3ap  11713  resinval  11714  recosval  11715  efi4p  11716  efival  11731  efmival  11732  efeul  11733  sinadd  11735  cosadd  11736  tanaddap  11738  sinsub  11739  cossub  11740  sincossq  11747  sin2t  11748  cos2t  11749  cos2tsin  11750  ef01bndlem  11755  sin01bnd  11756  cos01bnd  11757  cos12dec  11766  absef  11768  absefib  11769  efieq1re  11770  demoivreALT  11772  eirraplem  11775  dvdsexp  11857  oexpneg  11872  opeo  11892  omeo  11893  m1exp1  11896  flodddiv4  11929  flodddiv4t2lthalf  11932  divgcdnnr  11967  gcdaddm  11975  gcdadd  11976  gcdid  11977  modgcd  11982  gcdmultipled  11984  dvdsgcdidd  11985  bezoutlemnewy  11987  bezoutlema  11990  bezoutlemb  11991  bezoutlemex  11992  bezoutlembz  11995  absmulgcd  12008  gcdmultiple  12011  gcdmultiplez  12012  rpmulgcd  12017  rplpwr  12018  eucalginv  12046  eucalg  12049  lcmneg  12064  lcmgcdlem  12067  lcmgcd  12068  lcmid  12070  lcm1  12071  mulgcddvds  12084  qredeq  12086  divgcdcoprmex  12092  prmind2  12110  rpexp1i  12144  pw2dvdslemn  12155  pw2dvdseulemle  12157  pw2dvdseu  12158  oddpwdclemxy  12159  oddpwdclemdvds  12160  oddpwdclemndvds  12161  oddpwdclemdc  12163  2sqpwodd  12166  nn0gcdsq  12190  phiprmpw  12212  eulerthlemrprm  12219  eulerthlema  12220  eulerthlemh  12221  eulerthlemth  12222  fermltl  12224  prmdiv  12225  hashgcdlem  12228  odzdvds  12235  vfermltl  12241  modprm0  12244  nnnn0modprm0  12245  modprmn0modprm0  12246  coprimeprodsq  12247  pythagtriplem1  12255  pythagtriplem4  12258  pythagtriplem12  12265  pythagtriplem14  12267  pythagtriplem16  12269  pythagtriplem18  12271  pythagtrip  12273  pcpremul  12283  pceu  12285  pczpre  12287  pcdiv  12292  pcqmul  12293  pcqdiv  12297  pcexp  12299  pczdvds  12303  pczndvds  12305  pczndvds2  12307  pcid  12313  pcneg  12314  pcdvdstr  12316  pcgcd1  12317  pcgcd  12318  pc2dvds  12319  pcaddlem  12328  pcadd  12329  pcmpt  12331  pcmpt2  12332  fldivp1  12336  pcfac  12338  pcbc  12339  expnprm  12341  prmpwdvds  12343  pockthlem  12344  pockthi  12346  4sqlem7  12372  4sqlem9  12374  4sqlem10  12375  4sqlem2  12377  4sqlem3  12378  4sqlem4  12380  mul4sqlem  12381  setscomd  12493  ressvalsets  12514  strressid  12520  ressval3d  12521  ressinbasd  12523  ressressg  12524  ressabsg  12525  grprinvlem  12734  grprinvd  12735  grpridd  12736  isnsgrp  12742  sgrpass  12744  sgrp1  12746  mnd32g  12758  mnd4g  12760  mndpropd  12771  mhmlin  12786  grprcan  12838  grpsubval  12847  grpinvid2  12853  grpasscan2  12862  grpsubinv  12871  grpinvadd  12876  grpsubid1  12883  grpsubadd0sub  12885  grpsubadd  12886  grpsubsub  12887  grpaddsubass  12888  grppncan  12889  grpnnncan2  12895  grpsubpropd2  12903  mhmlem  12906  mhmid  12907  mhmmnd  12908  ghmgrp  12910  mulgnnp1  12919  mulgaddcomlem  12933  mulgaddcom  12934  mulginvinv  12936  mulgnn0dir  12940  mulgdirlem  12941  mulgp1  12943  mulgneg2  12944  mulgnn0ass  12946  mulgass  12947  mulgmodid  12949  mulgsubdir  12950  ablsub4  13016  abladdsub4  13017  ablsubsub4  13022  ablsub32  13025  ablnnncan  13026  mgpress  13041  srgass  13054  srgpcomp  13073  srgpcompp  13074  srgpcomppsc  13075  srg1expzeq1  13078  ringpropd  13117  ringrz  13123  rngnegr  13129  ringmneg2  13131  ringsubdi  13133  rngsubdir  13134  ring1  13136  opprring  13148  mulgass3  13153  dvdsrd  13162  unitgrp  13184  invrfvald  13190  dvr1  13206  dvrass  13207  dvrcan1  13208  dvrcan3  13209  rdivmuldivd  13212  cnfldsub  13274  restabs  13457  cnprcl2k  13488  cnrest2r  13519  ispsmet  13605  psmettri2  13610  psmetsym  13611  ismet  13626  isxmet  13627  xmettri2  13643  xmetsym  13650  xmettri3  13656  mettri3  13657  xblss2ps  13686  xblss2  13687  comet  13781  xmetxp  13789  xmetxpbl  13790  txmetcnp  13800  fsumcncntop  13838  cncfi  13847  limccl  13910  ellimc3apf  13911  limccnpcntop  13926  limccnp2lem  13927  reldvg  13930  dvfvalap  13932  eldvap  13933  dvcj  13955  dvfre  13956  dvexp  13957  dvexp2  13958  dvrecap  13959  dvmptaddx  13963  dvmptmulx  13964  dvmptnegcn  13966  dvmptsubcn  13967  dvmptcjx  13968  dveflem  13969  dvef  13970  sin0pilem1  13984  sin0pilem2  13985  efper  14010  sinperlem  14011  efimpi  14022  ptolemy  14027  tangtx  14041  abssinper  14049  cosq34lt1  14053  rpcxpef  14097  rpcxpp1  14109  rpcxpneg  14110  rpcxpsub  14111  rpmulcxp  14112  rpdivcxp  14114  cxpmul  14115  rpcxproot  14116  cxpcom  14139  rpabscxpbnd  14141  rplogbval  14145  rplogbreexp  14153  rplogbzexp  14154  rprelogbmulexp  14156  rprelogbdiv  14157  relogbexpap  14158  rplogbcxp  14163  rpcxplogb  14164  logbgcd1irr  14167  logbgcd1irraplemap  14169  binom4  14179  lgslem1  14183  lgsval  14187  lgsfvalg  14188  lgsval2lem  14193  lgsval4  14203  lgsneg  14207  lgsneg1  14208  lgsmod  14209  lgsdir2  14216  lgsdirprm  14217  lgsdilem2  14219  lgsdi  14220  lgsne0  14221  lgssq2  14224  lgsdirnn0  14230  lgsdinn0  14231  2sqlem2  14233  2sqlem3  14235  2sqlem4  14236  2sqlem8  14241  2sqlem9  14242  2sqlem10  14243  qdencn  14546  trilpolemclim  14555  trilpolemcl  14556  trilpolemisumle  14557  trilpolemeq1  14559  trilpolemlt1  14560  trilpo  14562  apdifflemf  14565  apdiff  14567  iswomni0  14570  redcwlpolemeq1  14573  redcwlpo  14574  nconstwlpolem0  14581  nconstwlpolemgt0  14582  nconstwlpo  14584  neapmkv  14586