Theorem oveq2d 6095

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 6087	. 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 1402  (class class class)co 6079

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 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 theorem depends on definitions:  df-bi 117  df-3an 1011  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-v 2823  df-un 3224  df-sn 3714  df-pr 3715  df-op 3717  df-uni 3934  df-br 4129  df-iota 5335  df-fv 5383  df-ov 6082

This theorem is referenced by:  csbov1g  6120  caovassg  6242  caovdig  6258  caovdirg  6261  caov32d  6264  caov4d  6268  caov42d  6270  suppofss1dcl  6498  suppofss2dcl  6499  nnaass  6752  nndi  6753  nnmass  6754  nnmsucr  6755  ecovass  6912  ecoviass  6913  ecovdi  6914  ecovidi  6915  addasspig  7691  mulasspig  7693  distrpig  7694  dfplpq2  7715  mulpipq2  7732  addassnqg  7743  prarloclemarch  7779  prarloclemarch2  7780  ltrnqg  7781  enq0sym  7793  addnq0mo  7808  mulnq0mo  7809  addnnnq0  7810  nq0a0  7818  distrnq0  7820  addassnq0  7823  prarloclemlo  7855  prarloclem3  7858  prarloclem5  7861  prarloclemcalc  7863  addnqprl  7890  addnqpru  7891  prmuloclemcalc  7926  mulnqprl  7929  mulnqpru  7930  distrlem4prl  7945  distrlem4pru  7946  1idprl  7951  1idpru  7952  ltexprlemloc  7968  addcanprleml  7975  addcanprlemu  7976  recexprlem1ssu  7995  ltmprr  8003  caucvgprlemcanl  8005  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  cauappcvgprlem1  8020  cauappcvgprlemlim  8022  caucvgprlemnkj  8027  caucvgprlemnbj  8028  caucvgprlemdisj  8035  caucvgprlemloc  8036  caucvgprlemcl  8037  caucvgprlemladdrl  8039  caucvgprlem1  8040  caucvgpr  8043  caucvgprprlemell  8046  caucvgprprlemcbv  8048  caucvgprprlemval  8049  caucvgprprlemnkeqj  8051  caucvgprprlemopl  8058  caucvgprprlemlol  8059  caucvgprprlemloc  8064  caucvgprprlemclphr  8066  caucvgprprlemexb  8068  caucvgprprlemaddq  8069  caucvgprprlem1  8070  addcmpblnr  8100  mulcmpblnrlemg  8101  addsrmo  8104  mulsrmo  8105  addsrpr  8106  mulsrpr  8107  ltsrprg  8108  recexgt0sr  8134  mulgt0sr  8139  caucvgsrlemgt1  8156  caucvgsrlemoffval  8157  caucvgsr  8163  suplocsrlemb  8167  suplocsrlempr  8168  suplocsrlem  8169  suplocsr  8170  mulcnsr  8196  pitoregt0  8210  recidpirqlemcalc  8218  axmulcom  8232  axmulass  8234  axdistr  8235  ax0id  8239  axcnre  8242  recriota  8251  axcaucvglemcau  8259  axcaucvglemres  8260  mulrid  8317  adddirp1d  8346  mul32  8450  mul31  8451  add32  8479  add4  8481  add42  8482  cnegex  8498  addcan2  8501  addsubass  8530  subsub2  8548  nppcan2  8551  sub32  8554  nnncan  8555  sub4  8565  muladd  8705  subdi  8706  mul2neg  8719  submul2  8720  mulsub  8722  muls1d  8739  mulsubfacd  8740  add20  8796  recexre  8900  rereim  8908  apreap  8909  ltmul1  8914  cru  8924  apreim  8925  mulreim  8926  apadd1  8930  apneg  8933  mulap0  8976  divrecap  9012  divassap  9014  divmulasscomap  9020  divsubdirap  9032  divdivdivap  9037  divmul24ap  9040  divmuleqap  9041  divcanap6  9043  divdivap1  9047  divdivap2  9048  divsubdivap  9052  conjmulap  9053  div2negap  9059  apmul1  9112  cju  9285  nnmulcl  9308  add1p1  9538  sub1m1  9539  cnm2m1cnm3  9540  xp1d2m1eqxm1d2  9541  div4p1lem1div2  9542  un0addcl  9579  un0mulcl  9580  zaddcllemneg  9666  qapne  10022  cnref1o  10034  rexsub  10238  xnegid  10244  xaddcom  10246  xnegdi  10253  xaddass  10254  xaddass2  10255  xpncan  10256  xnpcan  10257  xleadd1a  10258  xsubge0  10266  xposdif  10267  xlesubadd  10268  xadd4d  10270  lincmb01cmp  10388  iccf1o  10390  ige3m2fz  10437  fztp  10468  fzsuc2  10469  fseq1m1p1  10485  fzm1  10490  ige2m1fz1  10499  nn0split  10526  nnsplit  10527  fzo0addelr  10590  elfzoext  10593  fzval3  10605  zpnn0elfzo1  10609  fzosplitsnm1  10610  fzosplitpr  10635  fzosplitprm1  10636  fzoshftral  10640  rebtwn2zlemstep  10670  flhalf  10720  fldiv4lem1div2uz2  10724  modqval  10744  modqvalr  10745  modqdiffl  10755  modqfrac  10757  flqmod  10758  intqfrac  10759  zmod10  10760  modqmulnn  10762  modqvalp1  10763  modqid  10769  modqcyc  10779  modqcyc2  10780  modqmul1  10797  q2submod  10805  modqdi  10812  modqsubdir  10813  modqeqmodmin  10814  modsumfzodifsn  10816  addmodlteq  10818  frecuzrdgsuctlem  10843  uzsinds  10864  seqeq3  10872  iseqvalcbv  10879  seq3val  10880  seqvalcd  10881  seqf  10884  seq3p1  10885  seqovcd  10887  seqp1cd  10890  seq3m1  10893  seq3fveq2  10895  seqfveq2g  10897  seq3shft2  10901  seqshft2g  10902  monoord2  10906  ser3mono  10907  seq3split  10908  seqsplitg  10909  seq3caopr3  10911  seqcaopr3g  10912  seq3caopr2  10913  seqcaopr2g  10914  seq3caopr  10915  seqcaoprg  10916  seqf1oglem2a  10938  seqf1oglem2  10940  seq3id2  10946  seq3homo  10947  seq3z  10948  seqhomog  10950  exp3vallem  10960  exp3val  10961  expp1  10966  expnegap0  10967  expineg2  10968  expn1ap0  10969  expm1t  10987  1exp  10988  expnegzap  10993  mulexpzap  10999  expadd  11001  expaddzaplem  11002  expaddzap  11003  expmul  11004  expmulzap  11005  m1expeven  11006  expsubap  11007  expp1zap  11008  expm1ap  11009  expdivap  11010  iexpcyc  11064  subsq2  11067  binom2  11071  binom21  11072  binom2sub  11073  binom2sub1  11074  mulbinom2  11076  binom3  11077  zesq  11079  bernneq  11081  sqoddm1div8  11114  mulsubdivbinom2ap  11132  nn0opthlem1d  11141  nn0opthd  11143  facp1  11151  facnn2  11155  faclbnd  11162  faclbnd6  11165  bcval  11170  bccmpl  11175  bcn0  11176  bcnn  11178  bcnp1n  11180  bcm1k  11181  bcp1n  11182  bcp1nk  11183  bcval5  11184  bcp1m1  11186  bcpasc  11187  bcm1n  11190  bcn2m1  11191  bcn2p1  11192  omgadd  11225  hashunlem  11227  hashunsng  11231  hashdifsn  11243  hashxp  11250  hashmap  11251  sseqn  11262  hashf1lem2  11269  hashf1  11270  hashfac  11271  zfz1isolemsplit  11273  zfz1isolem1  11275  zfz1iso  11276  seq3coll  11277  wrdf  11293  ccatfvalfi  11343  elfzelfzccat  11351  ccatlid  11357  ccatrid  11358  ccatass  11359  ccatalpha  11364  ccatws1leng  11385  ccats1val2  11391  ccatw2s1p1g  11396  swrdval  11403  swrd00g  11404  swrdf  11410  swrdfv2  11418  swrdwrdsymbg  11419  swrdspsleq  11422  swrds1  11423  swrdlsw  11424  ccatswrd  11425  swrdccat2  11426  pfxmpt  11435  pfxfv  11439  pfxeq  11451  pfxsuff1eqwrdeq  11454  ccatpfx  11456  pfxccat1  11457  swrdswrd  11460  pfxswrd  11461  swrdpfx  11462  pfxpfx  11463  pfxlswccat  11468  ccats1pfxeq  11469  ccats1pfxeqrex  11470  ccatopth2  11472  cats1un  11476  wrdind  11477  wrd2ind  11478  swrdccatfn  11479  swrdccatin1  11480  pfxccatin12lem4  11481  swrdccatin2  11484  pfxccatin12lem2c  11485  pfxccatin12lem2  11486  pfxccatin12  11488  swrdccat  11490  swrdccat3blem  11494  swrdccat3b  11495  swrdccatin2d  11499  pfxccatin12d  11500  reuccatpfxs1lem  11501  reuccatpfxs1  11502  shftcan1  11582  shftcan2  11583  cjval  11593  cjth  11594  crre  11605  replim  11607  remim  11608  reim0b  11610  rereb  11611  mulreap  11612  cjreb  11614  recj  11615  reneg  11616  readd  11617  resub  11618  remullem  11619  imcj  11623  imneg  11624  imadd  11625  imsub  11626  cjcj  11631  cjadd  11632  ipcnval  11634  cjmulrcl  11635  cjneg  11638  addcj  11639  cjsub  11640  sq01  11643  cnrecnv  11659  caucvgrelemcau  11729  cvg1nlemcau  11733  cvg1nlemres  11734  recvguniqlem  11743  resqrexlemover  11759  resqrexlemlo  11762  resqrexlemcalc1  11763  resqrexlemcalc3  11765  resqrexlemnm  11767  resqrexlemcvg  11768  absneg  11799  abscj  11801  sqabsadd  11804  sqabssub  11805  absmul  11818  absid  11820  absre  11826  absresq  11827  absexpzap  11829  recvalap  11846  abstri  11853  abs2dif2  11856  recan  11858  cau3lem  11863  amgm2  11867  bdtrilem  11988  xrmaxadd  12010  xrbdtri  12025  climaddc1  12078  climsubc1  12081  climcvg1nlem  12098  serf0  12101  fzf1o  12125  summodclem3  12130  summodclem2a  12131  summodc  12133  fsumsplitsn  12160  fsumm1  12166  fsumsplitsnun  12169  fsump1  12170  isummulc2  12176  fsumrev  12193  fisum0diag2  12197  fsummulc2  12198  fsumsub  12202  fsumabs  12215  telfsumo  12216  fsumparts  12220  fsumrelem  12221  fsumiun  12227  binomlem  12233  binom  12234  binom1p  12235  binom11  12236  binom1dif  12237  bcxmas  12239  isumsplit  12241  isum1p  12242  divcnv  12247  arisum2  12249  trireciplem  12250  trirecip  12251  geolim  12261  georeclim  12263  geo2sum  12264  geo2lim  12266  geoisum1c  12270  0.999...  12271  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  cvgratz  12282  mertenslem2  12286  mertensabs  12287  clim2prod  12289  prodfrecap  12296  prodfdivap  12297  prodmodclem3  12325  prodmodclem2a  12326  fprodm1  12348  fprodp1  12350  fprodunsn  12354  fprodfac  12365  fprodeq0  12367  fprodconst  12370  fprodrec  12379  fproddivap  12380  fprodsplitsn  12383  ege2le3  12421  efaddlem  12424  efsub  12431  efexp  12432  eftlub  12440  efsep  12441  effsumlt  12442  ef4p  12444  tanval3ap  12464  resinval  12465  recosval  12466  efi4p  12467  efival  12482  efmival  12483  efeul  12484  sinadd  12486  cosadd  12487  tanaddap  12489  sinsub  12490  cossub  12491  sincossq  12498  sin2t  12499  cos2t  12500  cos2tsin  12501  ef01bndlem  12506  sin01bnd  12507  cos01bnd  12508  cos12dec  12518  absef  12520  absefib  12521  efieq1re  12522  demoivreALT  12524  eirraplem  12527  dvdsexp  12611  oexpneg  12627  opeo  12647  omeo  12648  m1exp1  12651  flodddiv4  12686  flodddiv4t2lthalf  12689  bitsval  12693  bitsp1  12701  bitsinv1lem  12711  bitsinv1  12712  divgcdnnr  12736  gcdaddm  12744  gcdadd  12745  gcdid  12746  modgcd  12751  gcdmultipled  12753  dvdsgcdidd  12754  bezoutlemnewy  12756  bezoutlema  12759  bezoutlemb  12760  bezoutlemex  12761  bezoutlembz  12764  absmulgcd  12777  gcdmultiple  12780  gcdmultiplez  12781  rpmulgcd  12786  rplpwr  12787  eucalginv  12817  eucalg  12820  lcmneg  12835  lcmgcdlem  12838  lcmgcd  12839  lcmid  12841  lcm1  12842  mulgcddvds  12855  qredeq  12857  divgcdcoprmex  12863  prmind2  12881  rpexp1i  12915  pw2dvdslemn  12926  pw2dvdseulemle  12928  pw2dvdseu  12929  oddpwdclemxy  12930  oddpwdclemdvds  12931  oddpwdclemndvds  12932  oddpwdclemdc  12934  2sqpwodd  12937  nn0gcdsq  12961  phiprmpw  12983  eulerthlemrprm  12990  eulerthlema  12991  eulerthlemh  12992  eulerthlemth  12993  fermltl  12995  prmdiv  12996  hashgcdlem  12999  odzdvds  13007  vfermltl  13013  modprm0  13016  nnnn0modprm0  13017  modprmn0modprm0  13018  coprimeprodsq  13019  pythagtriplem1  13027  pythagtriplem4  13030  pythagtriplem12  13037  pythagtriplem14  13039  pythagtriplem16  13041  pythagtriplem18  13043  pythagtrip  13045  pcpremul  13055  pceu  13057  pczpre  13059  pcdiv  13064  pcqmul  13065  pcqdiv  13069  pcexp  13071  pcxqcl  13074  pczdvds  13076  pczndvds  13078  pczndvds2  13080  pcid  13086  pcneg  13087  pcdvdstr  13089  pcgcd1  13090  pcgcd  13091  pc2dvds  13092  pcaddlem  13101  pcadd  13102  pcadd2  13103  pcmpt  13105  pcmpt2  13106  fldivp1  13110  pcfac  13112  pcbc  13113  expnprm  13115  prmpwdvds  13117  pockthlem  13118  pockthi  13120  4sqlem7  13146  4sqlem9  13148  4sqlem10  13149  4sqlem2  13151  4sqlem3  13152  4sqlem4  13154  mul4sqlem  13155  4sqlem11  13163  4sqlem16  13168  4sqlem17  13169  4sqlem19  13171  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilemsv  13236  ballotfilemsima  13242  ballotfilemfrci  13254  setscomd  13376  ressvalsets  13401  strressid  13408  ressval3d  13409  ressinbasd  13411  ressressg  13412  ressabsg  13413  grpinvalem  13688  grpinva  13689  grprida  13690  isnsgrp  13704  sgrpass  13706  sgrp1  13709  sgrppropd  13711  mnd32g  13723  mnd4g  13725  mndpropd  13736  imasmnd2  13742  mhmex  13752  mhmlin  13757  gzsumwmhm  13786  grprcan  13825  grpsubval  13834  grpinvid2  13841  grpasscan2  13852  grpsubinv  13861  grpinvadd  13866  grpsubid1  13873  grpsubadd0sub  13875  grpsubadd  13876  grpsubsub  13877  grpaddsubass  13878  grppncan  13879  grpnnncan2  13885  grpsubpropd2  13893  imasgrp2  13896  mhmlem  13900  mhmid  13901  mhmmnd  13902  ghmgrp  13904  mulgnn0gzsum  13914  mulgnnp1  13916  mulgaddcomlem  13931  mulgaddcom  13932  mulginvinv  13934  mulgnn0dir  13938  mulgdirlem  13939  mulgp1  13941  mulgneg2  13942  mulgnn0ass  13944  mulgass  13945  mulgmodid  13947  mulgsubdir  13948  nmzsubg  13996  0nsg  14000  eqger  14010  qussub  14023  ghmlin  14034  ghmsub  14037  conjghm  14062  ablsub4  14100  abladdsub4  14101  ablsubsub4  14106  ablsub32  14109  ablnnncan  14110  gzsumconst  14126  gzsummhm2  14129  gzsumsnfd  14130  gzsumsplit0  14131  gsumvalfi  14135  gzsumgsum1  14136  gzsumgsum  14138  gsumsncmn  14139  gsump1  14140  gsumzfi  14141  gsumclfi  14142  gsumf1ofi  14143  gsummptfidmadd  14144  gsummptfidmadd2  14145  gsumsubmclfi  14146  gsummhm2fi  14148  gsumconstcmn  14149  prdssgrpd  14174  prdsidlem  14176  prdsmndd  14177  mgpress  14213  rngass  14221  rngdi  14222  rngdir  14223  rngrz  14228  rngmneg2  14230  rngsubdi  14233  rngsubdir  14234  rngpropd  14237  imasrng  14238  srgass  14258  srgpcomp  14277  srgpcompp  14278  srgpcomppsc  14279  srg1expzeq1  14282  ringpropd  14326  ringrz  14332  ringnegr  14340  ringmneg2  14342  ringsubdi  14344  ringsubdir  14345  ring1  14347  imasring  14352  opprrng  14365  opprring  14367  mulgass3  14374  dvdsrd  14384  unitgrp  14406  invrfvald  14412  dvr1  14428  dvrass  14429  dvrcan1  14430  dvrcan3  14431  rdivmuldivd  14434  subrginv  14528  subrgdv  14529  resrhm2b  14540  rrgsupp  14557  islmod  14610  lmodlema  14611  islmodd  14612  lmodvs0  14642  lmodvneg1  14650  lmodvsubval2  14662  lmodsubvs  14663  lmodsubdi  14664  lmodsubdir  14665  lmodprop2d  14668  rmodislmodlem  14670  rmodislmod  14671  lsssn0  14690  sraval  14757  cnfldsub  14895  gsumfsum  14906  mulgrhm  14927  mulgrhm2  14928  znval  14954  znval2  14956  znunit  14977  isassa  14985  assalem  14986  assa2ass2  14993  assapropd  14997  asclmul1  15012  asclmul2  15013  ascldimul  15014  asclpropd  15023  assamulgscmlem2  15025  asclmulg  15027  psrval  15033  mplvalcoe  15064  mplval2g  15069  restabs  15259  cnprcl2k  15290  cnrest2r  15321  ispsmet  15407  psmettri2  15412  psmetsym  15413  ismet  15428  isxmet  15429  xmettri2  15445  xmetsym  15452  xmettri3  15458  mettri3  15459  xblss2ps  15488  xblss2  15489  comet  15583  xmetxp  15591  xmetxpbl  15592  txmetcnp  15602  fsumcncntop  15651  cncfi  15662  divcncfap  15698  limccl  15743  ellimc3apf  15744  limccnpcntop  15759  limccnp2lem  15760  reldvg  15763  dvfvalap  15765  eldvap  15766  dvcj  15793  dvfre  15794  dvexp  15795  dvexp2  15796  dvrecap  15797  dvmptaddx  15803  dvmptmulx  15804  dvmptnegcn  15806  dvmptsubcn  15807  dvmptcjx  15808  dvmptfsum  15809  dveflem  15810  dvef  15811  plyconst  15829  plyaddlem1  15831  plymullem1  15832  plyadd  15835  plymul  15836  plycoeid3  15841  plycolemc  15842  plyco  15843  plycjlemc  15844  plycj  15845  plyrecj  15847  dvply1  15849  dvply2g  15850  sin0pilem1  15865  sin0pilem2  15866  efper  15891  sinperlem  15892  efimpi  15903  ptolemy  15908  tangtx  15922  abssinper  15930  cosq34lt1  15934  rpcxpef  15979  rpcxpp1  15991  rpcxpneg  15992  rpcxpsub  15993  rpmulcxp  15994  rpdivcxp  15996  cxpmul  15997  rpcxpmul2  15998  rpcxproot  15999  cxpcom  16023  rpabscxpbnd  16025  rplogbval  16030  rplogbreexp  16038  rplogbzexp  16039  rprelogbmulexp  16041  rprelogbdiv  16042  relogbexpap  16043  rplogbcxp  16048  rpcxplogb  16049  logbgcd1irr  16052  logbgcd1irraplemap  16054  binom4  16064  log2tlbndlog2  16065  log2ublem2  16067  birthdaylem2  16071  pellexlem2  16075  pellexlem3  16076  wilthlem1  16077  sgmval  16080  sgmppw  16089  1sgmprm  16091  mersenne  16094  perfectlem1  16096  perfectlem2  16097  perfect  16098  lgslem1  16102  lgsval  16106  lgsfvalg  16107  lgsval2lem  16112  lgsval4  16122  lgsneg  16126  lgsneg1  16127  lgsmod  16128  lgsdir2  16135  lgsdirprm  16136  lgsdilem2  16138  lgsdi  16139  lgsne0  16140  lgssq2  16143  lgsdirnn0  16149  lgsdinn0  16150  gausslemma2dlem1a  16160  gausslemma2dlem1f1o  16162  gausslemma2dlem2  16164  gausslemma2dlem3  16165  gausslemma2dlem4  16166  gausslemma2dlem5  16168  gausslemma2dlem6  16169  gausslemma2d  16171  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem3  16174  lgseisenlem4  16175  lgsquadlem1  16179  lgsquadlem2  16180  lgsquadlem3  16181  lgsquad2lem1  16183  lgsquad2lem2  16184  lgsquad2  16185  lgsquad3  16186  m1lgs  16187  2lgslem3c  16197  2lgslem3d  16198  2lgslem3d1  16202  2sqlem2  16217  2sqlem3  16219  2sqlem4  16220  2sqlem8  16225  2sqlem9  16226  2sqlem10  16227  vtxdumgrfival  16522  p1evtxdeqfi  16536  p1evtxdp1fi  16537  iswlk  16547  upgr2wlkdc  16601  wlkres  16603  trlreslem  16613  isclwwlk  16618  clwwlkccatlem  16624  clwwlknp  16641  clwwlkn1  16642  clwwlkn2  16645  clwwlkext2edg  16646  clwwlknonex2lem1  16661  clwwlknonex2lem2  16662  clwwlknonex2  16663  iseupth  16671  eupth2lem3lem6fi  16695  eupth2lem3lem4fi  16697  depindlem1  16730  qdencn  17046  trilpolemclim  17059  trilpolemcl  17060  trilpolemisumle  17061  trilpolemeq1  17063  trilpolemlt1  17064  trilpo  17066  apdifflemf  17069  apdiff  17071  iswomni0  17075  redcwlpolemeq1  17078  redcwlpo  17079  nconstwlpolem0  17087  nconstwlpolemgt0  17088  nconstwlpo  17090  neapmkv  17092