Theorem oveq2d 6026

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 6018	. 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 1395  (class class class)co 6010

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5281  df-fv 5329  df-ov 6013

This theorem is referenced by:  csbov1g  6051  caovassg  6173  caovdig  6189  caovdirg  6192  caov32d  6195  caov4d  6199  caov42d  6201  nnaass  6644  nndi  6645  nnmass  6646  nnmsucr  6647  ecovass  6804  ecoviass  6805  ecovdi  6806  ecovidi  6807  addasspig  7533  mulasspig  7535  distrpig  7536  dfplpq2  7557  mulpipq2  7574  addassnqg  7585  prarloclemarch  7621  prarloclemarch2  7622  ltrnqg  7623  enq0sym  7635  addnq0mo  7650  mulnq0mo  7651  addnnnq0  7652  nq0a0  7660  distrnq0  7662  addassnq0  7665  prarloclemlo  7697  prarloclem3  7700  prarloclem5  7703  prarloclemcalc  7705  addnqprl  7732  addnqpru  7733  prmuloclemcalc  7768  mulnqprl  7771  mulnqpru  7772  distrlem4prl  7787  distrlem4pru  7788  1idprl  7793  1idpru  7794  ltexprlemloc  7810  addcanprleml  7817  addcanprlemu  7818  recexprlem1ssu  7837  ltmprr  7845  caucvgprlemcanl  7847  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  cauappcvgprlem1  7862  cauappcvgprlemlim  7864  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemdisj  7877  caucvgprlemloc  7878  caucvgprlemcl  7879  caucvgprlemladdrl  7881  caucvgprlem1  7882  caucvgpr  7885  caucvgprprlemell  7888  caucvgprprlemcbv  7890  caucvgprprlemval  7891  caucvgprprlemnkeqj  7893  caucvgprprlemopl  7900  caucvgprprlemlol  7901  caucvgprprlemloc  7906  caucvgprprlemclphr  7908  caucvgprprlemexb  7910  caucvgprprlemaddq  7911  caucvgprprlem1  7912  addcmpblnr  7942  mulcmpblnrlemg  7943  addsrmo  7946  mulsrmo  7947  addsrpr  7948  mulsrpr  7949  ltsrprg  7950  recexgt0sr  7976  mulgt0sr  7981  caucvgsrlemgt1  7998  caucvgsrlemoffval  7999  caucvgsr  8005  suplocsrlemb  8009  suplocsrlempr  8010  suplocsrlem  8011  suplocsr  8012  mulcnsr  8038  pitoregt0  8052  recidpirqlemcalc  8060  axmulcom  8074  axmulass  8076  axdistr  8077  ax0id  8081  axcnre  8084  recriota  8093  axcaucvglemcau  8101  axcaucvglemres  8102  mulrid  8159  adddirp1d  8189  mul32  8292  mul31  8293  add32  8321  add4  8323  add42  8324  cnegex  8340  addcan2  8343  addsubass  8372  subsub2  8390  nppcan2  8393  sub32  8396  nnncan  8397  sub4  8407  muladd  8546  subdi  8547  mul2neg  8560  submul2  8561  mulsub  8563  muls1d  8580  mulsubfacd  8581  add20  8637  recexre  8741  rereim  8749  apreap  8750  ltmul1  8755  cru  8765  apreim  8766  mulreim  8767  apadd1  8771  apneg  8774  mulap0  8817  divrecap  8851  divassap  8853  divmulasscomap  8859  divsubdirap  8871  divdivdivap  8876  divmul24ap  8879  divmuleqap  8880  divcanap6  8882  divdivap1  8886  divdivap2  8887  divsubdivap  8891  conjmulap  8892  div2negap  8898  apmul1  8951  cju  9124  nnmulcl  9147  add1p1  9377  sub1m1  9378  cnm2m1cnm3  9379  xp1d2m1eqxm1d2  9380  div4p1lem1div2  9381  un0addcl  9418  un0mulcl  9419  zaddcllemneg  9501  qapne  9851  cnref1o  9863  rexsub  10066  xnegid  10072  xaddcom  10074  xnegdi  10081  xaddass  10082  xaddass2  10083  xpncan  10084  xnpcan  10085  xleadd1a  10086  xsubge0  10094  xposdif  10095  xlesubadd  10096  xadd4d  10098  lincmb01cmp  10216  iccf1o  10217  ige3m2fz  10262  fztp  10291  fzsuc2  10292  fseq1m1p1  10308  fzm1  10313  ige2m1fz1  10322  nn0split  10349  nnsplit  10350  fzo0addelr  10412  elfzoext  10415  fzval3  10427  zpnn0elfzo1  10431  fzosplitsnm1  10432  fzosplitprm1  10457  fzoshftral  10461  rebtwn2zlemstep  10489  flhalf  10539  fldiv4lem1div2uz2  10543  modqval  10563  modqvalr  10564  modqdiffl  10574  modqfrac  10576  flqmod  10577  intqfrac  10578  zmod10  10579  modqmulnn  10581  modqvalp1  10582  modqid  10588  modqcyc  10598  modqcyc2  10599  modqmul1  10616  q2submod  10624  modqdi  10631  modqsubdir  10632  modqeqmodmin  10633  modsumfzodifsn  10635  addmodlteq  10637  frecuzrdgsuctlem  10662  uzsinds  10683  seqeq3  10691  iseqvalcbv  10698  seq3val  10699  seqvalcd  10700  seqf  10703  seq3p1  10704  seqovcd  10706  seqp1cd  10709  seq3m1  10712  seq3fveq2  10714  seqfveq2g  10716  seq3shft2  10720  seqshft2g  10721  monoord2  10725  ser3mono  10726  seq3split  10727  seqsplitg  10728  seq3caopr3  10730  seqcaopr3g  10731  seq3caopr2  10732  seqcaopr2g  10733  seq3caopr  10734  seqcaoprg  10735  seqf1oglem2a  10757  seqf1oglem2  10759  seq3id2  10765  seq3homo  10766  seq3z  10767  seqhomog  10769  exp3vallem  10779  exp3val  10780  expp1  10785  expnegap0  10786  expineg2  10787  expn1ap0  10788  expm1t  10806  1exp  10807  expnegzap  10812  mulexpzap  10818  expadd  10820  expaddzaplem  10821  expaddzap  10822  expmul  10823  expmulzap  10824  m1expeven  10825  expsubap  10826  expp1zap  10827  expm1ap  10828  expdivap  10829  iexpcyc  10883  subsq2  10886  binom2  10890  binom21  10891  binom2sub  10892  binom2sub1  10893  mulbinom2  10895  binom3  10896  zesq  10897  bernneq  10899  sqoddm1div8  10932  mulsubdivbinom2ap  10950  nn0opthlem1d  10959  nn0opthd  10961  facp1  10969  facnn2  10973  faclbnd  10980  faclbnd6  10983  bcval  10988  bccmpl  10993  bcn0  10994  bcnn  10996  bcnp1n  10998  bcm1k  10999  bcp1n  11000  bcp1nk  11001  bcval5  11002  bcp1m1  11004  bcpasc  11005  bcn2m1  11008  bcn2p1  11009  omgadd  11041  hashunlem  11043  hashunsng  11047  hashdifsn  11059  hashxp  11066  zfz1isolemsplit  11078  zfz1isolem1  11080  zfz1iso  11081  seq3coll  11082  wrdf  11095  ccatfvalfi  11145  elfzelfzccat  11153  ccatlid  11159  ccatrid  11160  ccatass  11161  ccatalpha  11166  ccatws1leng  11187  ccats1val2  11192  swrdval  11201  swrd00g  11202  swrdf  11208  swrdfv2  11216  swrdwrdsymbg  11217  swrdspsleq  11220  swrds1  11221  swrdlsw  11222  ccatswrd  11223  swrdccat2  11224  pfxmpt  11233  pfxfv  11237  pfxeq  11249  pfxsuff1eqwrdeq  11252  ccatpfx  11254  pfxccat1  11255  swrdswrd  11258  pfxswrd  11259  swrdpfx  11260  pfxpfx  11261  pfxlswccat  11266  ccats1pfxeq  11267  ccats1pfxeqrex  11268  ccatopth2  11270  cats1un  11274  wrdind  11275  wrd2ind  11276  swrdccatfn  11277  swrdccatin1  11278  pfxccatin12lem4  11279  swrdccatin2  11282  pfxccatin12lem2c  11283  pfxccatin12lem2  11284  pfxccatin12  11286  swrdccat  11288  swrdccat3blem  11292  swrdccat3b  11293  swrdccatin2d  11297  pfxccatin12d  11298  reuccatpfxs1lem  11299  reuccatpfxs1  11300  shftcan1  11366  shftcan2  11367  cjval  11377  cjth  11378  crre  11389  replim  11391  remim  11392  reim0b  11394  rereb  11395  mulreap  11396  cjreb  11398  recj  11399  reneg  11400  readd  11401  resub  11402  remullem  11403  imcj  11407  imneg  11408  imadd  11409  imsub  11410  cjcj  11415  cjadd  11416  ipcnval  11418  cjmulrcl  11419  cjneg  11422  addcj  11423  cjsub  11424  cnrecnv  11442  caucvgrelemcau  11512  cvg1nlemcau  11516  cvg1nlemres  11517  recvguniqlem  11526  resqrexlemover  11542  resqrexlemlo  11545  resqrexlemcalc1  11546  resqrexlemcalc3  11548  resqrexlemnm  11550  resqrexlemcvg  11551  absneg  11582  abscj  11584  sqabsadd  11587  sqabssub  11588  absmul  11601  absid  11603  absre  11609  absresq  11610  absexpzap  11612  recvalap  11629  abstri  11636  abs2dif2  11639  recan  11641  cau3lem  11646  amgm2  11650  bdtrilem  11771  xrmaxadd  11793  xrbdtri  11808  climaddc1  11861  climsubc1  11864  climcvg1nlem  11881  serf0  11884  summodclem3  11912  summodclem2a  11913  summodc  11915  fsumsplitsn  11942  fsumm1  11948  fsumsplitsnun  11951  fsump1  11952  isummulc2  11958  fsumrev  11975  fisum0diag2  11979  fsummulc2  11980  fsumsub  11984  fsumabs  11997  telfsumo  11998  fsumparts  12002  fsumrelem  12003  fsumiun  12009  binomlem  12015  binom  12016  binom1p  12017  binom11  12018  binom1dif  12019  bcxmas  12021  isumsplit  12023  isum1p  12024  divcnv  12029  arisum2  12031  trireciplem  12032  trirecip  12033  geolim  12043  georeclim  12045  geo2sum  12046  geo2lim  12048  geoisum1c  12052  0.999...  12053  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  cvgratz  12064  mertenslem2  12068  mertensabs  12069  clim2prod  12071  prodfrecap  12078  prodfdivap  12079  prodmodclem3  12107  prodmodclem2a  12108  fprodm1  12130  fprodp1  12132  fprodunsn  12136  fprodfac  12147  fprodeq0  12149  fprodconst  12152  fprodrec  12161  fproddivap  12162  fprodsplitsn  12165  ege2le3  12203  efaddlem  12206  efsub  12213  efexp  12214  eftlub  12222  efsep  12223  effsumlt  12224  ef4p  12226  tanval3ap  12246  resinval  12247  recosval  12248  efi4p  12249  efival  12264  efmival  12265  efeul  12266  sinadd  12268  cosadd  12269  tanaddap  12271  sinsub  12272  cossub  12273  sincossq  12280  sin2t  12281  cos2t  12282  cos2tsin  12283  ef01bndlem  12288  sin01bnd  12289  cos01bnd  12290  cos12dec  12300  absef  12302  absefib  12303  efieq1re  12304  demoivreALT  12306  eirraplem  12309  dvdsexp  12393  oexpneg  12409  opeo  12429  omeo  12430  m1exp1  12433  flodddiv4  12468  flodddiv4t2lthalf  12471  bitsval  12475  bitsp1  12483  bitsinv1lem  12493  bitsinv1  12494  divgcdnnr  12518  gcdaddm  12526  gcdadd  12527  gcdid  12528  modgcd  12533  gcdmultipled  12535  dvdsgcdidd  12536  bezoutlemnewy  12538  bezoutlema  12541  bezoutlemb  12542  bezoutlemex  12543  bezoutlembz  12546  absmulgcd  12559  gcdmultiple  12562  gcdmultiplez  12563  rpmulgcd  12568  rplpwr  12569  eucalginv  12599  eucalg  12602  lcmneg  12617  lcmgcdlem  12620  lcmgcd  12621  lcmid  12623  lcm1  12624  mulgcddvds  12637  qredeq  12639  divgcdcoprmex  12645  prmind2  12663  rpexp1i  12697  pw2dvdslemn  12708  pw2dvdseulemle  12710  pw2dvdseu  12711  oddpwdclemxy  12712  oddpwdclemdvds  12713  oddpwdclemndvds  12714  oddpwdclemdc  12716  2sqpwodd  12719  nn0gcdsq  12743  phiprmpw  12765  eulerthlemrprm  12772  eulerthlema  12773  eulerthlemh  12774  eulerthlemth  12775  fermltl  12777  prmdiv  12778  hashgcdlem  12781  odzdvds  12789  vfermltl  12795  modprm0  12798  nnnn0modprm0  12799  modprmn0modprm0  12800  coprimeprodsq  12801  pythagtriplem1  12809  pythagtriplem4  12812  pythagtriplem12  12819  pythagtriplem14  12821  pythagtriplem16  12823  pythagtriplem18  12825  pythagtrip  12827  pcpremul  12837  pceu  12839  pczpre  12841  pcdiv  12846  pcqmul  12847  pcqdiv  12851  pcexp  12853  pcxqcl  12856  pczdvds  12858  pczndvds  12860  pczndvds2  12862  pcid  12868  pcneg  12869  pcdvdstr  12871  pcgcd1  12872  pcgcd  12873  pc2dvds  12874  pcaddlem  12883  pcadd  12884  pcadd2  12885  pcmpt  12887  pcmpt2  12888  fldivp1  12892  pcfac  12894  pcbc  12895  expnprm  12897  prmpwdvds  12899  pockthlem  12900  pockthi  12902  4sqlem7  12928  4sqlem9  12930  4sqlem10  12931  4sqlem2  12933  4sqlem3  12934  4sqlem4  12936  mul4sqlem  12937  4sqlem11  12945  4sqlem16  12950  4sqlem17  12951  4sqlem19  12953  setscomd  13094  ressvalsets  13118  strressid  13125  ressval3d  13126  ressinbasd  13128  ressressg  13129  ressabsg  13130  grpinvalem  13439  grpinva  13440  grprida  13441  isnsgrp  13460  sgrpass  13462  sgrp1  13465  sgrppropd  13467  prdssgrpd  13469  mnd32g  13481  mnd4g  13483  mndpropd  13494  prdsidlem  13501  prdsmndd  13502  imasmnd2  13506  mhmex  13516  mhmlin  13521  gsumwmhm  13552  grprcan  13591  grpsubval  13600  grpinvid2  13607  grpasscan2  13618  grpsubinv  13627  grpinvadd  13632  grpsubid1  13639  grpsubadd0sub  13641  grpsubadd  13642  grpsubsub  13643  grpaddsubass  13644  grppncan  13645  grpnnncan2  13651  grpsubpropd2  13659  imasgrp2  13668  mhmlem  13672  mhmid  13673  mhmmnd  13674  ghmgrp  13676  mulgnn0gsum  13686  mulgnnp1  13688  mulgaddcomlem  13703  mulgaddcom  13704  mulginvinv  13706  mulgnn0dir  13710  mulgdirlem  13711  mulgp1  13713  mulgneg2  13714  mulgnn0ass  13716  mulgass  13717  mulgmodid  13719  mulgsubdir  13720  nmzsubg  13768  0nsg  13772  eqger  13782  qussub  13795  ghmlin  13806  ghmsub  13809  conjghm  13834  ablsub4  13871  abladdsub4  13872  ablsubsub4  13877  ablsub32  13880  ablnnncan  13881  gsumfzmptfidmadd2  13898  gsumfzconst  13899  gsumfzmhm2  13902  gsumfzsnfd  13903  mgpress  13915  rngass  13923  rngdi  13924  rngdir  13925  rngrz  13930  rngmneg2  13932  rngsubdi  13935  rngsubdir  13936  rngpropd  13939  imasrng  13940  srgass  13955  srgpcomp  13974  srgpcompp  13975  srgpcomppsc  13976  srg1expzeq1  13979  ringpropd  14022  ringrz  14028  ringnegr  14036  ringmneg2  14038  ringsubdi  14040  ringsubdir  14041  ring1  14043  imasring  14048  opprrng  14061  opprring  14063  mulgass3  14069  dvdsrd  14079  unitgrp  14101  invrfvald  14107  dvr1  14123  dvrass  14124  dvrcan1  14125  dvrcan3  14126  rdivmuldivd  14129  subrginv  14222  subrgdv  14223  resrhm2b  14234  islmod  14276  lmodlema  14277  islmodd  14278  lmodvs0  14307  lmodvneg1  14315  lmodvsubval2  14327  lmodsubvs  14328  lmodsubdi  14329  lmodsubdir  14330  lmodprop2d  14333  rmodislmodlem  14335  rmodislmod  14336  lsssn0  14355  sraval  14422  cnfldsub  14560  gsumfzfsumlem0  14571  gsumfzfsumlemm  14572  mulgrhm  14594  mulgrhm2  14595  znval  14621  znval2  14623  znunit  14644  psrval  14651  mplvalcoe  14675  mplval2g  14680  restabs  14870  cnprcl2k  14901  cnrest2r  14932  ispsmet  15018  psmettri2  15023  psmetsym  15024  ismet  15039  isxmet  15040  xmettri2  15056  xmetsym  15063  xmettri3  15069  mettri3  15070  xblss2ps  15099  xblss2  15100  comet  15194  xmetxp  15202  xmetxpbl  15203  txmetcnp  15213  fsumcncntop  15262  cncfi  15273  divcncfap  15309  limccl  15354  ellimc3apf  15355  limccnpcntop  15370  limccnp2lem  15371  reldvg  15374  dvfvalap  15376  eldvap  15377  dvcj  15404  dvfre  15405  dvexp  15406  dvexp2  15407  dvrecap  15408  dvmptaddx  15414  dvmptmulx  15415  dvmptnegcn  15417  dvmptsubcn  15418  dvmptcjx  15419  dvmptfsum  15420  dveflem  15421  dvef  15422  plyconst  15440  plyaddlem1  15442  plymullem1  15443  plyadd  15446  plymul  15447  plycoeid3  15452  plycolemc  15453  plyco  15454  plycjlemc  15455  plycj  15456  plyrecj  15458  dvply1  15460  dvply2g  15461  sin0pilem1  15476  sin0pilem2  15477  efper  15502  sinperlem  15503  efimpi  15514  ptolemy  15519  tangtx  15533  abssinper  15541  cosq34lt1  15545  rpcxpef  15589  rpcxpp1  15601  rpcxpneg  15602  rpcxpsub  15603  rpmulcxp  15604  rpdivcxp  15606  cxpmul  15607  rpcxpmul2  15608  rpcxproot  15609  cxpcom  15633  rpabscxpbnd  15635  rplogbval  15640  rplogbreexp  15648  rplogbzexp  15649  rprelogbmulexp  15651  rprelogbdiv  15652  relogbexpap  15653  rplogbcxp  15658  rpcxplogb  15659  logbgcd1irr  15662  logbgcd1irraplemap  15664  binom4  15674  wilthlem1  15675  sgmval  15678  sgmppw  15687  1sgmprm  15689  mersenne  15692  perfectlem1  15694  perfectlem2  15695  perfect  15696  lgslem1  15700  lgsval  15704  lgsfvalg  15705  lgsval2lem  15710  lgsval4  15720  lgsneg  15724  lgsneg1  15725  lgsmod  15726  lgsdir2  15733  lgsdirprm  15734  lgsdilem2  15736  lgsdi  15737  lgsne0  15738  lgssq2  15741  lgsdirnn0  15747  lgsdinn0  15748  gausslemma2dlem1a  15758  gausslemma2dlem1f1o  15760  gausslemma2dlem2  15762  gausslemma2dlem3  15763  gausslemma2dlem4  15764  gausslemma2dlem5  15766  gausslemma2dlem6  15767  gausslemma2d  15769  lgseisenlem1  15770  lgseisenlem2  15771  lgseisenlem3  15772  lgseisenlem4  15773  lgsquadlem1  15777  lgsquadlem2  15778  lgsquadlem3  15779  lgsquad2lem1  15781  lgsquad2lem2  15782  lgsquad2  15783  lgsquad3  15784  m1lgs  15785  2lgslem3c  15795  2lgslem3d  15796  2lgslem3d1  15800  2sqlem2  15815  2sqlem3  15817  2sqlem4  15818  2sqlem8  15823  2sqlem9  15824  2sqlem10  15825  vtxdumgrfival  16084  iswlk  16095  upgr2wlkdc  16147  wlkres  16149  trlreslem  16158  isclwwlk  16163  clwwlkccatlem  16169  clwwlknp  16185  clwwlkn1  16186  clwwlkn2  16189  clwwlkext2edg  16190  qdencn  16509  trilpolemclim  16518  trilpolemcl  16519  trilpolemisumle  16520  trilpolemeq1  16522  trilpolemlt1  16523  trilpo  16525  apdifflemf  16528  apdiff  16530  iswomni0  16533  redcwlpolemeq1  16536  redcwlpo  16537  nconstwlpolem0  16545  nconstwlpolemgt0  16546  nconstwlpo  16548  neapmkv  16550