Theorem oveq2d 6034

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 6026	. 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 1397  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  csbov1g  6059  caovassg  6181  caovdig  6197  caovdirg  6200  caov32d  6203  caov4d  6207  caov42d  6209  nnaass  6653  nndi  6654  nnmass  6655  nnmsucr  6656  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  addasspig  7550  mulasspig  7552  distrpig  7553  dfplpq2  7574  mulpipq2  7591  addassnqg  7602  prarloclemarch  7638  prarloclemarch2  7639  ltrnqg  7640  enq0sym  7652  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  nq0a0  7677  distrnq0  7679  addassnq0  7682  prarloclemlo  7714  prarloclem3  7717  prarloclem5  7720  prarloclemcalc  7722  addnqprl  7749  addnqpru  7750  prmuloclemcalc  7785  mulnqprl  7788  mulnqpru  7789  distrlem4prl  7804  distrlem4pru  7805  1idprl  7810  1idpru  7811  ltexprlemloc  7827  addcanprleml  7834  addcanprlemu  7835  recexprlem1ssu  7854  ltmprr  7862  caucvgprlemcanl  7864  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  cauappcvgprlem1  7879  cauappcvgprlemlim  7881  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemdisj  7894  caucvgprlemloc  7895  caucvgprlemcl  7896  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgpr  7902  caucvgprprlemell  7905  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemnkeqj  7910  caucvgprprlemopl  7917  caucvgprprlemlol  7918  caucvgprprlemloc  7923  caucvgprprlemclphr  7925  caucvgprprlemexb  7927  caucvgprprlemaddq  7928  caucvgprprlem1  7929  addcmpblnr  7959  mulcmpblnrlemg  7960  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  ltsrprg  7967  recexgt0sr  7993  mulgt0sr  7998  caucvgsrlemgt1  8015  caucvgsrlemoffval  8016  caucvgsr  8022  suplocsrlemb  8026  suplocsrlempr  8027  suplocsrlem  8028  suplocsr  8029  mulcnsr  8055  pitoregt0  8069  recidpirqlemcalc  8077  axmulcom  8091  axmulass  8093  axdistr  8094  ax0id  8098  axcnre  8101  recriota  8110  axcaucvglemcau  8118  axcaucvglemres  8119  mulrid  8176  adddirp1d  8206  mul32  8309  mul31  8310  add32  8338  add4  8340  add42  8341  cnegex  8357  addcan2  8360  addsubass  8389  subsub2  8407  nppcan2  8410  sub32  8413  nnncan  8414  sub4  8424  muladd  8563  subdi  8564  mul2neg  8577  submul2  8578  mulsub  8580  muls1d  8597  mulsubfacd  8598  add20  8654  recexre  8758  rereim  8766  apreap  8767  ltmul1  8772  cru  8782  apreim  8783  mulreim  8784  apadd1  8788  apneg  8791  mulap0  8834  divrecap  8868  divassap  8870  divmulasscomap  8876  divsubdirap  8888  divdivdivap  8893  divmul24ap  8896  divmuleqap  8897  divcanap6  8899  divdivap1  8903  divdivap2  8904  divsubdivap  8908  conjmulap  8909  div2negap  8915  apmul1  8968  cju  9141  nnmulcl  9164  add1p1  9394  sub1m1  9395  cnm2m1cnm3  9396  xp1d2m1eqxm1d2  9397  div4p1lem1div2  9398  un0addcl  9435  un0mulcl  9436  zaddcllemneg  9518  qapne  9873  cnref1o  9885  rexsub  10088  xnegid  10094  xaddcom  10096  xnegdi  10103  xaddass  10104  xaddass2  10105  xpncan  10106  xnpcan  10107  xleadd1a  10108  xsubge0  10116  xposdif  10117  xlesubadd  10118  xadd4d  10120  lincmb01cmp  10238  iccf1o  10239  ige3m2fz  10284  fztp  10313  fzsuc2  10314  fseq1m1p1  10330  fzm1  10335  ige2m1fz1  10344  nn0split  10371  nnsplit  10372  fzo0addelr  10435  elfzoext  10438  fzval3  10450  zpnn0elfzo1  10454  fzosplitsnm1  10455  fzosplitpr  10480  fzosplitprm1  10481  fzoshftral  10485  rebtwn2zlemstep  10513  flhalf  10563  fldiv4lem1div2uz2  10567  modqval  10587  modqvalr  10588  modqdiffl  10598  modqfrac  10600  flqmod  10601  intqfrac  10602  zmod10  10603  modqmulnn  10605  modqvalp1  10606  modqid  10612  modqcyc  10622  modqcyc2  10623  modqmul1  10640  q2submod  10648  modqdi  10655  modqsubdir  10656  modqeqmodmin  10657  modsumfzodifsn  10659  addmodlteq  10661  frecuzrdgsuctlem  10686  uzsinds  10707  seqeq3  10715  iseqvalcbv  10722  seq3val  10723  seqvalcd  10724  seqf  10727  seq3p1  10728  seqovcd  10730  seqp1cd  10733  seq3m1  10736  seq3fveq2  10738  seqfveq2g  10740  seq3shft2  10744  seqshft2g  10745  monoord2  10749  ser3mono  10750  seq3split  10751  seqsplitg  10752  seq3caopr3  10754  seqcaopr3g  10755  seq3caopr2  10756  seqcaopr2g  10757  seq3caopr  10758  seqcaoprg  10759  seqf1oglem2a  10781  seqf1oglem2  10783  seq3id2  10789  seq3homo  10790  seq3z  10791  seqhomog  10793  exp3vallem  10803  exp3val  10804  expp1  10809  expnegap0  10810  expineg2  10811  expn1ap0  10812  expm1t  10830  1exp  10831  expnegzap  10836  mulexpzap  10842  expadd  10844  expaddzaplem  10845  expaddzap  10846  expmul  10847  expmulzap  10848  m1expeven  10849  expsubap  10850  expp1zap  10851  expm1ap  10852  expdivap  10853  iexpcyc  10907  subsq2  10910  binom2  10914  binom21  10915  binom2sub  10916  binom2sub1  10917  mulbinom2  10919  binom3  10920  zesq  10921  bernneq  10923  sqoddm1div8  10956  mulsubdivbinom2ap  10974  nn0opthlem1d  10983  nn0opthd  10985  facp1  10993  facnn2  10997  faclbnd  11004  faclbnd6  11007  bcval  11012  bccmpl  11017  bcn0  11018  bcnn  11020  bcnp1n  11022  bcm1k  11023  bcp1n  11024  bcp1nk  11025  bcval5  11026  bcp1m1  11028  bcpasc  11029  bcn2m1  11032  bcn2p1  11033  omgadd  11066  hashunlem  11068  hashunsng  11072  hashdifsn  11084  hashxp  11091  zfz1isolemsplit  11103  zfz1isolem1  11105  zfz1iso  11106  seq3coll  11107  wrdf  11120  ccatfvalfi  11170  elfzelfzccat  11178  ccatlid  11184  ccatrid  11185  ccatass  11186  ccatalpha  11191  ccatws1leng  11212  ccats1val2  11218  ccatw2s1p1g  11223  swrdval  11230  swrd00g  11231  swrdf  11237  swrdfv2  11245  swrdwrdsymbg  11246  swrdspsleq  11249  swrds1  11250  swrdlsw  11251  ccatswrd  11252  swrdccat2  11253  pfxmpt  11262  pfxfv  11266  pfxeq  11278  pfxsuff1eqwrdeq  11281  ccatpfx  11283  pfxccat1  11284  swrdswrd  11287  pfxswrd  11288  swrdpfx  11289  pfxpfx  11290  pfxlswccat  11295  ccats1pfxeq  11296  ccats1pfxeqrex  11297  ccatopth2  11299  cats1un  11303  wrdind  11304  wrd2ind  11305  swrdccatfn  11306  swrdccatin1  11307  pfxccatin12lem4  11308  swrdccatin2  11311  pfxccatin12lem2c  11312  pfxccatin12lem2  11313  pfxccatin12  11315  swrdccat  11317  swrdccat3blem  11321  swrdccat3b  11322  swrdccatin2d  11326  pfxccatin12d  11327  reuccatpfxs1lem  11328  reuccatpfxs1  11329  shftcan1  11396  shftcan2  11397  cjval  11407  cjth  11408  crre  11419  replim  11421  remim  11422  reim0b  11424  rereb  11425  mulreap  11426  cjreb  11428  recj  11429  reneg  11430  readd  11431  resub  11432  remullem  11433  imcj  11437  imneg  11438  imadd  11439  imsub  11440  cjcj  11445  cjadd  11446  ipcnval  11448  cjmulrcl  11449  cjneg  11452  addcj  11453  cjsub  11454  cnrecnv  11472  caucvgrelemcau  11542  cvg1nlemcau  11546  cvg1nlemres  11547  recvguniqlem  11556  resqrexlemover  11572  resqrexlemlo  11575  resqrexlemcalc1  11576  resqrexlemcalc3  11578  resqrexlemnm  11580  resqrexlemcvg  11581  absneg  11612  abscj  11614  sqabsadd  11617  sqabssub  11618  absmul  11631  absid  11633  absre  11639  absresq  11640  absexpzap  11642  recvalap  11659  abstri  11666  abs2dif2  11669  recan  11671  cau3lem  11676  amgm2  11680  bdtrilem  11801  xrmaxadd  11823  xrbdtri  11838  climaddc1  11891  climsubc1  11894  climcvg1nlem  11911  serf0  11914  fzf1o  11938  summodclem3  11943  summodclem2a  11944  summodc  11946  fsumsplitsn  11973  fsumm1  11979  fsumsplitsnun  11982  fsump1  11983  isummulc2  11989  fsumrev  12006  fisum0diag2  12010  fsummulc2  12011  fsumsub  12015  fsumabs  12028  telfsumo  12029  fsumparts  12033  fsumrelem  12034  fsumiun  12040  binomlem  12046  binom  12047  binom1p  12048  binom11  12049  binom1dif  12050  bcxmas  12052  isumsplit  12054  isum1p  12055  divcnv  12060  arisum2  12062  trireciplem  12063  trirecip  12064  geolim  12074  georeclim  12076  geo2sum  12077  geo2lim  12079  geoisum1c  12083  0.999...  12084  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  cvgratz  12095  mertenslem2  12099  mertensabs  12100  clim2prod  12102  prodfrecap  12109  prodfdivap  12110  prodmodclem3  12138  prodmodclem2a  12139  fprodm1  12161  fprodp1  12163  fprodunsn  12167  fprodfac  12178  fprodeq0  12180  fprodconst  12183  fprodrec  12192  fproddivap  12193  fprodsplitsn  12196  ege2le3  12234  efaddlem  12237  efsub  12244  efexp  12245  eftlub  12253  efsep  12254  effsumlt  12255  ef4p  12257  tanval3ap  12277  resinval  12278  recosval  12279  efi4p  12280  efival  12295  efmival  12296  efeul  12297  sinadd  12299  cosadd  12300  tanaddap  12302  sinsub  12303  cossub  12304  sincossq  12311  sin2t  12312  cos2t  12313  cos2tsin  12314  ef01bndlem  12319  sin01bnd  12320  cos01bnd  12321  cos12dec  12331  absef  12333  absefib  12334  efieq1re  12335  demoivreALT  12337  eirraplem  12340  dvdsexp  12424  oexpneg  12440  opeo  12460  omeo  12461  m1exp1  12464  flodddiv4  12499  flodddiv4t2lthalf  12502  bitsval  12506  bitsp1  12514  bitsinv1lem  12524  bitsinv1  12525  divgcdnnr  12549  gcdaddm  12557  gcdadd  12558  gcdid  12559  modgcd  12564  gcdmultipled  12566  dvdsgcdidd  12567  bezoutlemnewy  12569  bezoutlema  12572  bezoutlemb  12573  bezoutlemex  12574  bezoutlembz  12577  absmulgcd  12590  gcdmultiple  12593  gcdmultiplez  12594  rpmulgcd  12599  rplpwr  12600  eucalginv  12630  eucalg  12633  lcmneg  12648  lcmgcdlem  12651  lcmgcd  12652  lcmid  12654  lcm1  12655  mulgcddvds  12668  qredeq  12670  divgcdcoprmex  12676  prmind2  12694  rpexp1i  12728  pw2dvdslemn  12739  pw2dvdseulemle  12741  pw2dvdseu  12742  oddpwdclemxy  12743  oddpwdclemdvds  12744  oddpwdclemndvds  12745  oddpwdclemdc  12747  2sqpwodd  12750  nn0gcdsq  12774  phiprmpw  12796  eulerthlemrprm  12803  eulerthlema  12804  eulerthlemh  12805  eulerthlemth  12806  fermltl  12808  prmdiv  12809  hashgcdlem  12812  odzdvds  12820  vfermltl  12826  modprm0  12829  nnnn0modprm0  12830  modprmn0modprm0  12831  coprimeprodsq  12832  pythagtriplem1  12840  pythagtriplem4  12843  pythagtriplem12  12850  pythagtriplem14  12852  pythagtriplem16  12854  pythagtriplem18  12856  pythagtrip  12858  pcpremul  12868  pceu  12870  pczpre  12872  pcdiv  12877  pcqmul  12878  pcqdiv  12882  pcexp  12884  pcxqcl  12887  pczdvds  12889  pczndvds  12891  pczndvds2  12893  pcid  12899  pcneg  12900  pcdvdstr  12902  pcgcd1  12903  pcgcd  12904  pc2dvds  12905  pcaddlem  12914  pcadd  12915  pcadd2  12916  pcmpt  12918  pcmpt2  12919  fldivp1  12923  pcfac  12925  pcbc  12926  expnprm  12928  prmpwdvds  12930  pockthlem  12931  pockthi  12933  4sqlem7  12959  4sqlem9  12961  4sqlem10  12962  4sqlem2  12964  4sqlem3  12965  4sqlem4  12967  mul4sqlem  12968  4sqlem11  12976  4sqlem16  12981  4sqlem17  12982  4sqlem19  12984  setscomd  13125  ressvalsets  13149  strressid  13156  ressval3d  13157  ressinbasd  13159  ressressg  13160  ressabsg  13161  grpinvalem  13470  grpinva  13471  grprida  13472  isnsgrp  13491  sgrpass  13493  sgrp1  13496  sgrppropd  13498  prdssgrpd  13500  mnd32g  13512  mnd4g  13514  mndpropd  13525  prdsidlem  13532  prdsmndd  13533  imasmnd2  13537  mhmex  13547  mhmlin  13552  gsumwmhm  13583  grprcan  13622  grpsubval  13631  grpinvid2  13638  grpasscan2  13649  grpsubinv  13658  grpinvadd  13663  grpsubid1  13670  grpsubadd0sub  13672  grpsubadd  13673  grpsubsub  13674  grpaddsubass  13675  grppncan  13676  grpnnncan2  13682  grpsubpropd2  13690  imasgrp2  13699  mhmlem  13703  mhmid  13704  mhmmnd  13705  ghmgrp  13707  mulgnn0gsum  13717  mulgnnp1  13719  mulgaddcomlem  13734  mulgaddcom  13735  mulginvinv  13737  mulgnn0dir  13741  mulgdirlem  13742  mulgp1  13744  mulgneg2  13745  mulgnn0ass  13747  mulgass  13748  mulgmodid  13750  mulgsubdir  13751  nmzsubg  13799  0nsg  13803  eqger  13813  qussub  13826  ghmlin  13837  ghmsub  13840  conjghm  13865  ablsub4  13902  abladdsub4  13903  ablsubsub4  13908  ablsub32  13911  ablnnncan  13912  gsumfzmptfidmadd2  13929  gsumfzconst  13930  gsumfzmhm2  13933  gsumfzsnfd  13934  gsumsplit0  13935  mgpress  13947  rngass  13955  rngdi  13956  rngdir  13957  rngrz  13962  rngmneg2  13964  rngsubdi  13967  rngsubdir  13968  rngpropd  13971  imasrng  13972  srgass  13987  srgpcomp  14006  srgpcompp  14007  srgpcomppsc  14008  srg1expzeq1  14011  ringpropd  14054  ringrz  14060  ringnegr  14068  ringmneg2  14070  ringsubdi  14072  ringsubdir  14073  ring1  14075  imasring  14080  opprrng  14093  opprring  14095  mulgass3  14101  dvdsrd  14111  unitgrp  14133  invrfvald  14139  dvr1  14155  dvrass  14156  dvrcan1  14157  dvrcan3  14158  rdivmuldivd  14161  subrginv  14254  subrgdv  14255  resrhm2b  14266  islmod  14308  lmodlema  14309  islmodd  14310  lmodvs0  14339  lmodvneg1  14347  lmodvsubval2  14359  lmodsubvs  14360  lmodsubdi  14361  lmodsubdir  14362  lmodprop2d  14365  rmodislmodlem  14367  rmodislmod  14368  lsssn0  14387  sraval  14454  cnfldsub  14592  gsumfzfsumlem0  14603  gsumfzfsumlemm  14604  mulgrhm  14626  mulgrhm2  14627  znval  14653  znval2  14655  znunit  14676  psrval  14683  mplvalcoe  14707  mplval2g  14712  restabs  14902  cnprcl2k  14933  cnrest2r  14964  ispsmet  15050  psmettri2  15055  psmetsym  15056  ismet  15071  isxmet  15072  xmettri2  15088  xmetsym  15095  xmettri3  15101  mettri3  15102  xblss2ps  15131  xblss2  15132  comet  15226  xmetxp  15234  xmetxpbl  15235  txmetcnp  15245  fsumcncntop  15294  cncfi  15305  divcncfap  15341  limccl  15386  ellimc3apf  15387  limccnpcntop  15402  limccnp2lem  15403  reldvg  15406  dvfvalap  15408  eldvap  15409  dvcj  15436  dvfre  15437  dvexp  15438  dvexp2  15439  dvrecap  15440  dvmptaddx  15446  dvmptmulx  15447  dvmptnegcn  15449  dvmptsubcn  15450  dvmptcjx  15451  dvmptfsum  15452  dveflem  15453  dvef  15454  plyconst  15472  plyaddlem1  15474  plymullem1  15475  plyadd  15478  plymul  15479  plycoeid3  15484  plycolemc  15485  plyco  15486  plycjlemc  15487  plycj  15488  plyrecj  15490  dvply1  15492  dvply2g  15493  sin0pilem1  15508  sin0pilem2  15509  efper  15534  sinperlem  15535  efimpi  15546  ptolemy  15551  tangtx  15565  abssinper  15573  cosq34lt1  15577  rpcxpef  15621  rpcxpp1  15633  rpcxpneg  15634  rpcxpsub  15635  rpmulcxp  15636  rpdivcxp  15638  cxpmul  15639  rpcxpmul2  15640  rpcxproot  15641  cxpcom  15665  rpabscxpbnd  15667  rplogbval  15672  rplogbreexp  15680  rplogbzexp  15681  rprelogbmulexp  15683  rprelogbdiv  15684  relogbexpap  15685  rplogbcxp  15690  rpcxplogb  15691  logbgcd1irr  15694  logbgcd1irraplemap  15696  binom4  15706  wilthlem1  15707  sgmval  15710  sgmppw  15719  1sgmprm  15721  mersenne  15724  perfectlem1  15726  perfectlem2  15727  perfect  15728  lgslem1  15732  lgsval  15736  lgsfvalg  15737  lgsval2lem  15742  lgsval4  15752  lgsneg  15756  lgsneg1  15757  lgsmod  15758  lgsdir2  15765  lgsdirprm  15766  lgsdilem2  15768  lgsdi  15769  lgsne0  15770  lgssq2  15773  lgsdirnn0  15779  lgsdinn0  15780  gausslemma2dlem1a  15790  gausslemma2dlem1f1o  15792  gausslemma2dlem2  15794  gausslemma2dlem3  15795  gausslemma2dlem4  15796  gausslemma2dlem5  15798  gausslemma2dlem6  15799  gausslemma2d  15801  lgseisenlem1  15802  lgseisenlem2  15803  lgseisenlem3  15804  lgseisenlem4  15805  lgsquadlem1  15809  lgsquadlem2  15810  lgsquadlem3  15811  lgsquad2lem1  15813  lgsquad2lem2  15814  lgsquad2  15815  lgsquad3  15816  m1lgs  15817  2lgslem3c  15827  2lgslem3d  15828  2lgslem3d1  15832  2sqlem2  15847  2sqlem3  15849  2sqlem4  15850  2sqlem8  15855  2sqlem9  15856  2sqlem10  15857  vtxdumgrfival  16152  p1evtxdeqfi  16166  p1evtxdp1fi  16167  iswlk  16177  upgr2wlkdc  16231  wlkres  16233  trlreslem  16243  isclwwlk  16248  clwwlkccatlem  16254  clwwlknp  16271  clwwlkn1  16272  clwwlkn2  16275  clwwlkext2edg  16276  clwwlknonex2lem1  16291  clwwlknonex2lem2  16292  clwwlknonex2  16293  iseupth  16301  eupth2lem3lem6fi  16325  eupth2lem3lem4fi  16327  depindlem1  16346  qdencn  16652  trilpolemclim  16661  trilpolemcl  16662  trilpolemisumle  16663  trilpolemeq1  16665  trilpolemlt1  16666  trilpo  16668  apdifflemf  16671  apdiff  16673  iswomni0  16676  redcwlpolemeq1  16679  redcwlpo  16680  nconstwlpolem0  16688  nconstwlpolemgt0  16689  nconstwlpo  16691  neapmkv  16693  gfsumval  16701  gsumgfsum1  16702  gsumgfsum  16705  gfsumsn  16706  gfsump1  16707  gfsumcl  16708