Theorem oveq2d 6065

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 6057	. 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 1398  (class class class)co 6049

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2814  df-un 3214  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-br 4109  df-iota 5311  df-fv 5359  df-ov 6052

This theorem is referenced by:  csbov1g  6090  caovassg  6212  caovdig  6228  caovdirg  6231  caov32d  6234  caov4d  6238  caov42d  6240  suppofss1dcl  6463  suppofss2dcl  6464  nnaass  6717  nndi  6718  nnmass  6719  nnmsucr  6720  ecovass  6877  ecoviass  6878  ecovdi  6879  ecovidi  6880  addasspig  7641  mulasspig  7643  distrpig  7644  dfplpq2  7665  mulpipq2  7682  addassnqg  7693  prarloclemarch  7729  prarloclemarch2  7730  ltrnqg  7731  enq0sym  7743  addnq0mo  7758  mulnq0mo  7759  addnnnq0  7760  nq0a0  7768  distrnq0  7770  addassnq0  7773  prarloclemlo  7805  prarloclem3  7808  prarloclem5  7811  prarloclemcalc  7813  addnqprl  7840  addnqpru  7841  prmuloclemcalc  7876  mulnqprl  7879  mulnqpru  7880  distrlem4prl  7895  distrlem4pru  7896  1idprl  7901  1idpru  7902  ltexprlemloc  7918  addcanprleml  7925  addcanprlemu  7926  recexprlem1ssu  7945  ltmprr  7953  caucvgprlemcanl  7955  cauappcvgprlemladdru  7967  cauappcvgprlemladdrl  7968  cauappcvgprlem1  7970  cauappcvgprlemlim  7972  caucvgprlemnkj  7977  caucvgprlemnbj  7978  caucvgprlemdisj  7985  caucvgprlemloc  7986  caucvgprlemcl  7987  caucvgprlemladdrl  7989  caucvgprlem1  7990  caucvgpr  7993  caucvgprprlemell  7996  caucvgprprlemcbv  7998  caucvgprprlemval  7999  caucvgprprlemnkeqj  8001  caucvgprprlemopl  8008  caucvgprprlemlol  8009  caucvgprprlemloc  8014  caucvgprprlemclphr  8016  caucvgprprlemexb  8018  caucvgprprlemaddq  8019  caucvgprprlem1  8020  addcmpblnr  8050  mulcmpblnrlemg  8051  addsrmo  8054  mulsrmo  8055  addsrpr  8056  mulsrpr  8057  ltsrprg  8058  recexgt0sr  8084  mulgt0sr  8089  caucvgsrlemgt1  8106  caucvgsrlemoffval  8107  caucvgsr  8113  suplocsrlemb  8117  suplocsrlempr  8118  suplocsrlem  8119  suplocsr  8120  mulcnsr  8146  pitoregt0  8160  recidpirqlemcalc  8168  axmulcom  8182  axmulass  8184  axdistr  8185  ax0id  8189  axcnre  8192  recriota  8201  axcaucvglemcau  8209  axcaucvglemres  8210  mulrid  8267  adddirp1d  8296  mul32  8399  mul31  8400  add32  8428  add4  8430  add42  8431  cnegex  8447  addcan2  8450  addsubass  8479  subsub2  8497  nppcan2  8500  sub32  8503  nnncan  8504  sub4  8514  muladd  8653  subdi  8654  mul2neg  8667  submul2  8668  mulsub  8670  muls1d  8687  mulsubfacd  8688  add20  8744  recexre  8848  rereim  8856  apreap  8857  ltmul1  8862  cru  8872  apreim  8873  mulreim  8874  apadd1  8878  apneg  8881  mulap0  8924  divrecap  8958  divassap  8960  divmulasscomap  8966  divsubdirap  8978  divdivdivap  8983  divmul24ap  8986  divmuleqap  8987  divcanap6  8989  divdivap1  8993  divdivap2  8994  divsubdivap  8998  conjmulap  8999  div2negap  9005  apmul1  9058  cju  9231  nnmulcl  9254  add1p1  9484  sub1m1  9485  cnm2m1cnm3  9486  xp1d2m1eqxm1d2  9487  div4p1lem1div2  9488  un0addcl  9525  un0mulcl  9526  zaddcllemneg  9612  qapne  9967  cnref1o  9979  rexsub  10182  xnegid  10188  xaddcom  10190  xnegdi  10197  xaddass  10198  xaddass2  10199  xpncan  10200  xnpcan  10201  xleadd1a  10202  xsubge0  10210  xposdif  10211  xlesubadd  10212  xadd4d  10214  lincmb01cmp  10332  iccf1o  10334  ige3m2fz  10379  fztp  10408  fzsuc2  10409  fseq1m1p1  10425  fzm1  10430  ige2m1fz1  10439  nn0split  10466  nnsplit  10467  fzo0addelr  10530  elfzoext  10533  fzval3  10545  zpnn0elfzo1  10549  fzosplitsnm1  10550  fzosplitpr  10575  fzosplitprm1  10576  fzoshftral  10580  rebtwn2zlemstep  10608  flhalf  10658  fldiv4lem1div2uz2  10662  modqval  10682  modqvalr  10683  modqdiffl  10693  modqfrac  10695  flqmod  10696  intqfrac  10697  zmod10  10698  modqmulnn  10700  modqvalp1  10701  modqid  10707  modqcyc  10717  modqcyc2  10718  modqmul1  10735  q2submod  10743  modqdi  10750  modqsubdir  10751  modqeqmodmin  10752  modsumfzodifsn  10754  addmodlteq  10756  frecuzrdgsuctlem  10781  uzsinds  10802  seqeq3  10810  iseqvalcbv  10817  seq3val  10818  seqvalcd  10819  seqf  10822  seq3p1  10823  seqovcd  10825  seqp1cd  10828  seq3m1  10831  seq3fveq2  10833  seqfveq2g  10835  seq3shft2  10839  seqshft2g  10840  monoord2  10844  ser3mono  10845  seq3split  10846  seqsplitg  10847  seq3caopr3  10849  seqcaopr3g  10850  seq3caopr2  10851  seqcaopr2g  10852  seq3caopr  10853  seqcaoprg  10854  seqf1oglem2a  10876  seqf1oglem2  10878  seq3id2  10884  seq3homo  10885  seq3z  10886  seqhomog  10888  exp3vallem  10898  exp3val  10899  expp1  10904  expnegap0  10905  expineg2  10906  expn1ap0  10907  expm1t  10925  1exp  10926  expnegzap  10931  mulexpzap  10937  expadd  10939  expaddzaplem  10940  expaddzap  10941  expmul  10942  expmulzap  10943  m1expeven  10944  expsubap  10945  expp1zap  10946  expm1ap  10947  expdivap  10948  iexpcyc  11002  subsq2  11005  binom2  11009  binom21  11010  binom2sub  11011  binom2sub1  11012  mulbinom2  11014  binom3  11015  zesq  11016  bernneq  11018  sqoddm1div8  11051  mulsubdivbinom2ap  11069  nn0opthlem1d  11078  nn0opthd  11080  facp1  11088  facnn2  11092  faclbnd  11099  faclbnd6  11102  bcval  11107  bccmpl  11112  bcn0  11113  bcnn  11115  bcnp1n  11117  bcm1k  11118  bcp1n  11119  bcp1nk  11120  bcval5  11121  bcp1m1  11123  bcpasc  11124  bcn2m1  11127  bcn2p1  11128  omgadd  11161  hashunlem  11163  hashunsng  11167  hashdifsn  11179  hashxp  11186  sseqn  11196  zfz1isolemsplit  11203  zfz1isolem1  11205  zfz1iso  11206  seq3coll  11207  wrdf  11223  ccatfvalfi  11273  elfzelfzccat  11281  ccatlid  11287  ccatrid  11288  ccatass  11289  ccatalpha  11294  ccatws1leng  11315  ccats1val2  11321  ccatw2s1p1g  11326  swrdval  11333  swrd00g  11334  swrdf  11340  swrdfv2  11348  swrdwrdsymbg  11349  swrdspsleq  11352  swrds1  11353  swrdlsw  11354  ccatswrd  11355  swrdccat2  11356  pfxmpt  11365  pfxfv  11369  pfxeq  11381  pfxsuff1eqwrdeq  11384  ccatpfx  11386  pfxccat1  11387  swrdswrd  11390  pfxswrd  11391  swrdpfx  11392  pfxpfx  11393  pfxlswccat  11398  ccats1pfxeq  11399  ccats1pfxeqrex  11400  ccatopth2  11402  cats1un  11406  wrdind  11407  wrd2ind  11408  swrdccatfn  11409  swrdccatin1  11410  pfxccatin12lem4  11411  swrdccatin2  11414  pfxccatin12lem2c  11415  pfxccatin12lem2  11416  pfxccatin12  11418  swrdccat  11420  swrdccat3blem  11424  swrdccat3b  11425  swrdccatin2d  11429  pfxccatin12d  11430  reuccatpfxs1lem  11431  reuccatpfxs1  11432  shftcan1  11512  shftcan2  11513  cjval  11523  cjth  11524  crre  11535  replim  11537  remim  11538  reim0b  11540  rereb  11541  mulreap  11542  cjreb  11544  recj  11545  reneg  11546  readd  11547  resub  11548  remullem  11549  imcj  11553  imneg  11554  imadd  11555  imsub  11556  cjcj  11561  cjadd  11562  ipcnval  11564  cjmulrcl  11565  cjneg  11568  addcj  11569  cjsub  11570  cnrecnv  11588  caucvgrelemcau  11658  cvg1nlemcau  11662  cvg1nlemres  11663  recvguniqlem  11672  resqrexlemover  11688  resqrexlemlo  11691  resqrexlemcalc1  11692  resqrexlemcalc3  11694  resqrexlemnm  11696  resqrexlemcvg  11697  absneg  11728  abscj  11730  sqabsadd  11733  sqabssub  11734  absmul  11747  absid  11749  absre  11755  absresq  11756  absexpzap  11758  recvalap  11775  abstri  11782  abs2dif2  11785  recan  11787  cau3lem  11792  amgm2  11796  bdtrilem  11917  xrmaxadd  11939  xrbdtri  11954  climaddc1  12007  climsubc1  12010  climcvg1nlem  12027  serf0  12030  fzf1o  12054  summodclem3  12059  summodclem2a  12060  summodc  12062  fsumsplitsn  12089  fsumm1  12095  fsumsplitsnun  12098  fsump1  12099  isummulc2  12105  fsumrev  12122  fisum0diag2  12126  fsummulc2  12127  fsumsub  12131  fsumabs  12144  telfsumo  12145  fsumparts  12149  fsumrelem  12150  fsumiun  12156  binomlem  12162  binom  12163  binom1p  12164  binom11  12165  binom1dif  12166  bcxmas  12168  isumsplit  12170  isum1p  12171  divcnv  12176  arisum2  12178  trireciplem  12179  trirecip  12180  geolim  12190  georeclim  12192  geo2sum  12193  geo2lim  12195  geoisum1c  12199  0.999...  12200  cvgratnnlemnexp  12203  cvgratnnlemmn  12204  cvgratz  12211  mertenslem2  12215  mertensabs  12216  clim2prod  12218  prodfrecap  12225  prodfdivap  12226  prodmodclem3  12254  prodmodclem2a  12255  fprodm1  12277  fprodp1  12279  fprodunsn  12283  fprodfac  12294  fprodeq0  12296  fprodconst  12299  fprodrec  12308  fproddivap  12309  fprodsplitsn  12312  ege2le3  12350  efaddlem  12353  efsub  12360  efexp  12361  eftlub  12369  efsep  12370  effsumlt  12371  ef4p  12373  tanval3ap  12393  resinval  12394  recosval  12395  efi4p  12396  efival  12411  efmival  12412  efeul  12413  sinadd  12415  cosadd  12416  tanaddap  12418  sinsub  12419  cossub  12420  sincossq  12427  sin2t  12428  cos2t  12429  cos2tsin  12430  ef01bndlem  12435  sin01bnd  12436  cos01bnd  12437  cos12dec  12447  absef  12449  absefib  12450  efieq1re  12451  demoivreALT  12453  eirraplem  12456  dvdsexp  12540  oexpneg  12556  opeo  12576  omeo  12577  m1exp1  12580  flodddiv4  12615  flodddiv4t2lthalf  12618  bitsval  12622  bitsp1  12630  bitsinv1lem  12640  bitsinv1  12641  divgcdnnr  12665  gcdaddm  12673  gcdadd  12674  gcdid  12675  modgcd  12680  gcdmultipled  12682  dvdsgcdidd  12683  bezoutlemnewy  12685  bezoutlema  12688  bezoutlemb  12689  bezoutlemex  12690  bezoutlembz  12693  absmulgcd  12706  gcdmultiple  12709  gcdmultiplez  12710  rpmulgcd  12715  rplpwr  12716  eucalginv  12746  eucalg  12749  lcmneg  12764  lcmgcdlem  12767  lcmgcd  12768  lcmid  12770  lcm1  12771  mulgcddvds  12784  qredeq  12786  divgcdcoprmex  12792  prmind2  12810  rpexp1i  12844  pw2dvdslemn  12855  pw2dvdseulemle  12857  pw2dvdseu  12858  oddpwdclemxy  12859  oddpwdclemdvds  12860  oddpwdclemndvds  12861  oddpwdclemdc  12863  2sqpwodd  12866  nn0gcdsq  12890  phiprmpw  12912  eulerthlemrprm  12919  eulerthlema  12920  eulerthlemh  12921  eulerthlemth  12922  fermltl  12924  prmdiv  12925  hashgcdlem  12928  odzdvds  12936  vfermltl  12942  modprm0  12945  nnnn0modprm0  12946  modprmn0modprm0  12947  coprimeprodsq  12948  pythagtriplem1  12956  pythagtriplem4  12959  pythagtriplem12  12966  pythagtriplem14  12968  pythagtriplem16  12970  pythagtriplem18  12972  pythagtrip  12974  pcpremul  12984  pceu  12986  pczpre  12988  pcdiv  12993  pcqmul  12994  pcqdiv  12998  pcexp  13000  pcxqcl  13003  pczdvds  13005  pczndvds  13007  pczndvds2  13009  pcid  13015  pcneg  13016  pcdvdstr  13018  pcgcd1  13019  pcgcd  13020  pc2dvds  13021  pcaddlem  13030  pcadd  13031  pcadd2  13032  pcmpt  13034  pcmpt2  13035  fldivp1  13039  pcfac  13041  pcbc  13042  expnprm  13044  prmpwdvds  13046  pockthlem  13047  pockthi  13049  4sqlem7  13075  4sqlem9  13077  4sqlem10  13078  4sqlem2  13080  4sqlem3  13081  4sqlem4  13083  mul4sqlem  13084  4sqlem11  13092  4sqlem16  13097  4sqlem17  13098  4sqlem19  13100  setscomd  13242  ressvalsets  13266  strressid  13273  ressval3d  13274  ressinbasd  13276  ressressg  13277  ressabsg  13278  grpinvalem  13587  grpinva  13588  grprida  13589  isnsgrp  13608  sgrpass  13610  sgrp1  13613  sgrppropd  13615  prdssgrpd  13617  mnd32g  13629  mnd4g  13631  mndpropd  13642  prdsidlem  13649  prdsmndd  13650  imasmnd2  13654  mhmex  13664  mhmlin  13669  gsumwmhm  13700  grprcan  13739  grpsubval  13748  grpinvid2  13755  grpasscan2  13766  grpsubinv  13775  grpinvadd  13780  grpsubid1  13787  grpsubadd0sub  13789  grpsubadd  13790  grpsubsub  13791  grpaddsubass  13792  grppncan  13793  grpnnncan2  13799  grpsubpropd2  13807  imasgrp2  13816  mhmlem  13820  mhmid  13821  mhmmnd  13822  ghmgrp  13824  mulgnn0gsum  13834  mulgnnp1  13836  mulgaddcomlem  13851  mulgaddcom  13852  mulginvinv  13854  mulgnn0dir  13858  mulgdirlem  13859  mulgp1  13861  mulgneg2  13862  mulgnn0ass  13864  mulgass  13865  mulgmodid  13867  mulgsubdir  13868  nmzsubg  13916  0nsg  13920  eqger  13930  qussub  13943  ghmlin  13954  ghmsub  13957  conjghm  13982  ablsub4  14019  abladdsub4  14020  ablsubsub4  14025  ablsub32  14028  ablnnncan  14029  gsumfzmptfidmadd2  14046  gsumfzconst  14047  gsumfzmhm2  14050  gsumfzsnfd  14051  gsumsplit0  14052  mgpress  14064  rngass  14072  rngdi  14073  rngdir  14074  rngrz  14079  rngmneg2  14081  rngsubdi  14084  rngsubdir  14085  rngpropd  14088  imasrng  14089  srgass  14104  srgpcomp  14123  srgpcompp  14124  srgpcomppsc  14125  srg1expzeq1  14128  ringpropd  14171  ringrz  14177  ringnegr  14185  ringmneg2  14187  ringsubdi  14189  ringsubdir  14190  ring1  14192  imasring  14197  opprrng  14210  opprring  14212  mulgass3  14218  dvdsrd  14228  unitgrp  14250  invrfvald  14256  dvr1  14272  dvrass  14273  dvrcan1  14274  dvrcan3  14275  rdivmuldivd  14278  subrginv  14371  subrgdv  14372  resrhm2b  14383  rrgsupp  14400  islmod  14426  lmodlema  14427  islmodd  14428  lmodvs0  14457  lmodvneg1  14465  lmodvsubval2  14477  lmodsubvs  14478  lmodsubdi  14479  lmodsubdir  14480  lmodprop2d  14483  rmodislmodlem  14485  rmodislmod  14486  lsssn0  14505  sraval  14572  cnfldsub  14710  gsumfzfsumlem0  14721  gsumfzfsumlemm  14722  mulgrhm  14744  mulgrhm2  14745  znval  14771  znval2  14773  znunit  14794  psrval  14801  mplvalcoe  14832  mplval2g  14837  restabs  15027  cnprcl2k  15058  cnrest2r  15089  ispsmet  15175  psmettri2  15180  psmetsym  15181  ismet  15196  isxmet  15197  xmettri2  15213  xmetsym  15220  xmettri3  15226  mettri3  15227  xblss2ps  15256  xblss2  15257  comet  15351  xmetxp  15359  xmetxpbl  15360  txmetcnp  15370  fsumcncntop  15419  cncfi  15430  divcncfap  15466  limccl  15511  ellimc3apf  15512  limccnpcntop  15527  limccnp2lem  15528  reldvg  15531  dvfvalap  15533  eldvap  15534  dvcj  15561  dvfre  15562  dvexp  15563  dvexp2  15564  dvrecap  15565  dvmptaddx  15571  dvmptmulx  15572  dvmptnegcn  15574  dvmptsubcn  15575  dvmptcjx  15576  dvmptfsum  15577  dveflem  15578  dvef  15579  plyconst  15597  plyaddlem1  15599  plymullem1  15600  plyadd  15603  plymul  15604  plycoeid3  15609  plycolemc  15610  plyco  15611  plycjlemc  15612  plycj  15613  plyrecj  15615  dvply1  15617  dvply2g  15618  sin0pilem1  15633  sin0pilem2  15634  efper  15659  sinperlem  15660  efimpi  15671  ptolemy  15676  tangtx  15690  abssinper  15698  cosq34lt1  15702  rpcxpef  15746  rpcxpp1  15758  rpcxpneg  15759  rpcxpsub  15760  rpmulcxp  15761  rpdivcxp  15763  cxpmul  15764  rpcxpmul2  15765  rpcxproot  15766  cxpcom  15790  rpabscxpbnd  15792  rplogbval  15797  rplogbreexp  15805  rplogbzexp  15806  rprelogbmulexp  15808  rprelogbdiv  15809  relogbexpap  15810  rplogbcxp  15815  rpcxplogb  15816  logbgcd1irr  15819  logbgcd1irraplemap  15821  binom4  15831  pellexlem2  15833  pellexlem3  15834  wilthlem1  15835  sgmval  15838  sgmppw  15847  1sgmprm  15849  mersenne  15852  perfectlem1  15854  perfectlem2  15855  perfect  15856  lgslem1  15860  lgsval  15864  lgsfvalg  15865  lgsval2lem  15870  lgsval4  15880  lgsneg  15884  lgsneg1  15885  lgsmod  15886  lgsdir2  15893  lgsdirprm  15894  lgsdilem2  15896  lgsdi  15897  lgsne0  15898  lgssq2  15901  lgsdirnn0  15907  lgsdinn0  15908  gausslemma2dlem1a  15918  gausslemma2dlem1f1o  15920  gausslemma2dlem2  15922  gausslemma2dlem3  15923  gausslemma2dlem4  15924  gausslemma2dlem5  15926  gausslemma2dlem6  15927  gausslemma2d  15929  lgseisenlem1  15930  lgseisenlem2  15931  lgseisenlem3  15932  lgseisenlem4  15933  lgsquadlem1  15937  lgsquadlem2  15938  lgsquadlem3  15939  lgsquad2lem1  15941  lgsquad2lem2  15942  lgsquad2  15943  lgsquad3  15944  m1lgs  15945  2lgslem3c  15955  2lgslem3d  15956  2lgslem3d1  15960  2sqlem2  15975  2sqlem3  15977  2sqlem4  15978  2sqlem8  15983  2sqlem9  15984  2sqlem10  15985  vtxdumgrfival  16280  p1evtxdeqfi  16294  p1evtxdp1fi  16295  iswlk  16305  upgr2wlkdc  16359  wlkres  16361  trlreslem  16371  isclwwlk  16376  clwwlkccatlem  16382  clwwlknp  16399  clwwlkn1  16400  clwwlkn2  16403  clwwlkext2edg  16404  clwwlknonex2lem1  16419  clwwlknonex2lem2  16420  clwwlknonex2  16421  iseupth  16429  eupth2lem3lem6fi  16453  eupth2lem3lem4fi  16455  depindlem1  16488  qdencn  16794  trilpolemclim  16807  trilpolemcl  16808  trilpolemisumle  16809  trilpolemeq1  16811  trilpolemlt1  16812  trilpo  16814  apdifflemf  16817  apdiff  16819  iswomni0  16823  redcwlpolemeq1  16826  redcwlpo  16827  nconstwlpolem0  16835  nconstwlpolemgt0  16836  nconstwlpo  16838  neapmkv  16840  gfsumval  16848  gsumgfsum1  16849  gsumgfsum  16852  gfsumsn  16853  gfsump1  16854  gfsumz  16855  gfsumcl  16856