Theorem oveq2d 6029

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 6021	. 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 6013

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 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  csbov1g  6054  caovassg  6176  caovdig  6192  caovdirg  6195  caov32d  6198  caov4d  6202  caov42d  6204  nnaass  6648  nndi  6649  nnmass  6650  nnmsucr  6651  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  addasspig  7543  mulasspig  7545  distrpig  7546  dfplpq2  7567  mulpipq2  7584  addassnqg  7595  prarloclemarch  7631  prarloclemarch2  7632  ltrnqg  7633  enq0sym  7645  addnq0mo  7660  mulnq0mo  7661  addnnnq0  7662  nq0a0  7670  distrnq0  7672  addassnq0  7675  prarloclemlo  7707  prarloclem3  7710  prarloclem5  7713  prarloclemcalc  7715  addnqprl  7742  addnqpru  7743  prmuloclemcalc  7778  mulnqprl  7781  mulnqpru  7782  distrlem4prl  7797  distrlem4pru  7798  1idprl  7803  1idpru  7804  ltexprlemloc  7820  addcanprleml  7827  addcanprlemu  7828  recexprlem1ssu  7847  ltmprr  7855  caucvgprlemcanl  7857  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  cauappcvgprlem1  7872  cauappcvgprlemlim  7874  caucvgprlemnkj  7879  caucvgprlemnbj  7880  caucvgprlemdisj  7887  caucvgprlemloc  7888  caucvgprlemcl  7889  caucvgprlemladdrl  7891  caucvgprlem1  7892  caucvgpr  7895  caucvgprprlemell  7898  caucvgprprlemcbv  7900  caucvgprprlemval  7901  caucvgprprlemnkeqj  7903  caucvgprprlemopl  7910  caucvgprprlemlol  7911  caucvgprprlemloc  7916  caucvgprprlemclphr  7918  caucvgprprlemexb  7920  caucvgprprlemaddq  7921  caucvgprprlem1  7922  addcmpblnr  7952  mulcmpblnrlemg  7953  addsrmo  7956  mulsrmo  7957  addsrpr  7958  mulsrpr  7959  ltsrprg  7960  recexgt0sr  7986  mulgt0sr  7991  caucvgsrlemgt1  8008  caucvgsrlemoffval  8009  caucvgsr  8015  suplocsrlemb  8019  suplocsrlempr  8020  suplocsrlem  8021  suplocsr  8022  mulcnsr  8048  pitoregt0  8062  recidpirqlemcalc  8070  axmulcom  8084  axmulass  8086  axdistr  8087  ax0id  8091  axcnre  8094  recriota  8103  axcaucvglemcau  8111  axcaucvglemres  8112  mulrid  8169  adddirp1d  8199  mul32  8302  mul31  8303  add32  8331  add4  8333  add42  8334  cnegex  8350  addcan2  8353  addsubass  8382  subsub2  8400  nppcan2  8403  sub32  8406  nnncan  8407  sub4  8417  muladd  8556  subdi  8557  mul2neg  8570  submul2  8571  mulsub  8573  muls1d  8590  mulsubfacd  8591  add20  8647  recexre  8751  rereim  8759  apreap  8760  ltmul1  8765  cru  8775  apreim  8776  mulreim  8777  apadd1  8781  apneg  8784  mulap0  8827  divrecap  8861  divassap  8863  divmulasscomap  8869  divsubdirap  8881  divdivdivap  8886  divmul24ap  8889  divmuleqap  8890  divcanap6  8892  divdivap1  8896  divdivap2  8897  divsubdivap  8901  conjmulap  8902  div2negap  8908  apmul1  8961  cju  9134  nnmulcl  9157  add1p1  9387  sub1m1  9388  cnm2m1cnm3  9389  xp1d2m1eqxm1d2  9390  div4p1lem1div2  9391  un0addcl  9428  un0mulcl  9429  zaddcllemneg  9511  qapne  9866  cnref1o  9878  rexsub  10081  xnegid  10087  xaddcom  10089  xnegdi  10096  xaddass  10097  xaddass2  10098  xpncan  10099  xnpcan  10100  xleadd1a  10101  xsubge0  10109  xposdif  10110  xlesubadd  10111  xadd4d  10113  lincmb01cmp  10231  iccf1o  10232  ige3m2fz  10277  fztp  10306  fzsuc2  10307  fseq1m1p1  10323  fzm1  10328  ige2m1fz1  10337  nn0split  10364  nnsplit  10365  fzo0addelr  10427  elfzoext  10430  fzval3  10442  zpnn0elfzo1  10446  fzosplitsnm1  10447  fzosplitpr  10472  fzosplitprm1  10473  fzoshftral  10477  rebtwn2zlemstep  10505  flhalf  10555  fldiv4lem1div2uz2  10559  modqval  10579  modqvalr  10580  modqdiffl  10590  modqfrac  10592  flqmod  10593  intqfrac  10594  zmod10  10595  modqmulnn  10597  modqvalp1  10598  modqid  10604  modqcyc  10614  modqcyc2  10615  modqmul1  10632  q2submod  10640  modqdi  10647  modqsubdir  10648  modqeqmodmin  10649  modsumfzodifsn  10651  addmodlteq  10653  frecuzrdgsuctlem  10678  uzsinds  10699  seqeq3  10707  iseqvalcbv  10714  seq3val  10715  seqvalcd  10716  seqf  10719  seq3p1  10720  seqovcd  10722  seqp1cd  10725  seq3m1  10728  seq3fveq2  10730  seqfveq2g  10732  seq3shft2  10736  seqshft2g  10737  monoord2  10741  ser3mono  10742  seq3split  10743  seqsplitg  10744  seq3caopr3  10746  seqcaopr3g  10747  seq3caopr2  10748  seqcaopr2g  10749  seq3caopr  10750  seqcaoprg  10751  seqf1oglem2a  10773  seqf1oglem2  10775  seq3id2  10781  seq3homo  10782  seq3z  10783  seqhomog  10785  exp3vallem  10795  exp3val  10796  expp1  10801  expnegap0  10802  expineg2  10803  expn1ap0  10804  expm1t  10822  1exp  10823  expnegzap  10828  mulexpzap  10834  expadd  10836  expaddzaplem  10837  expaddzap  10838  expmul  10839  expmulzap  10840  m1expeven  10841  expsubap  10842  expp1zap  10843  expm1ap  10844  expdivap  10845  iexpcyc  10899  subsq2  10902  binom2  10906  binom21  10907  binom2sub  10908  binom2sub1  10909  mulbinom2  10911  binom3  10912  zesq  10913  bernneq  10915  sqoddm1div8  10948  mulsubdivbinom2ap  10966  nn0opthlem1d  10975  nn0opthd  10977  facp1  10985  facnn2  10989  faclbnd  10996  faclbnd6  10999  bcval  11004  bccmpl  11009  bcn0  11010  bcnn  11012  bcnp1n  11014  bcm1k  11015  bcp1n  11016  bcp1nk  11017  bcval5  11018  bcp1m1  11020  bcpasc  11021  bcn2m1  11024  bcn2p1  11025  omgadd  11058  hashunlem  11060  hashunsng  11064  hashdifsn  11076  hashxp  11083  zfz1isolemsplit  11095  zfz1isolem1  11097  zfz1iso  11098  seq3coll  11099  wrdf  11112  ccatfvalfi  11162  elfzelfzccat  11170  ccatlid  11176  ccatrid  11177  ccatass  11178  ccatalpha  11183  ccatws1leng  11204  ccats1val2  11210  ccatw2s1p1g  11215  swrdval  11222  swrd00g  11223  swrdf  11229  swrdfv2  11237  swrdwrdsymbg  11238  swrdspsleq  11241  swrds1  11242  swrdlsw  11243  ccatswrd  11244  swrdccat2  11245  pfxmpt  11254  pfxfv  11258  pfxeq  11270  pfxsuff1eqwrdeq  11273  ccatpfx  11275  pfxccat1  11276  swrdswrd  11279  pfxswrd  11280  swrdpfx  11281  pfxpfx  11282  pfxlswccat  11287  ccats1pfxeq  11288  ccats1pfxeqrex  11289  ccatopth2  11291  cats1un  11295  wrdind  11296  wrd2ind  11297  swrdccatfn  11298  swrdccatin1  11299  pfxccatin12lem4  11300  swrdccatin2  11303  pfxccatin12lem2c  11304  pfxccatin12lem2  11305  pfxccatin12  11307  swrdccat  11309  swrdccat3blem  11313  swrdccat3b  11314  swrdccatin2d  11318  pfxccatin12d  11319  reuccatpfxs1lem  11320  reuccatpfxs1  11321  shftcan1  11388  shftcan2  11389  cjval  11399  cjth  11400  crre  11411  replim  11413  remim  11414  reim0b  11416  rereb  11417  mulreap  11418  cjreb  11420  recj  11421  reneg  11422  readd  11423  resub  11424  remullem  11425  imcj  11429  imneg  11430  imadd  11431  imsub  11432  cjcj  11437  cjadd  11438  ipcnval  11440  cjmulrcl  11441  cjneg  11444  addcj  11445  cjsub  11446  cnrecnv  11464  caucvgrelemcau  11534  cvg1nlemcau  11538  cvg1nlemres  11539  recvguniqlem  11548  resqrexlemover  11564  resqrexlemlo  11567  resqrexlemcalc1  11568  resqrexlemcalc3  11570  resqrexlemnm  11572  resqrexlemcvg  11573  absneg  11604  abscj  11606  sqabsadd  11609  sqabssub  11610  absmul  11623  absid  11625  absre  11631  absresq  11632  absexpzap  11634  recvalap  11651  abstri  11658  abs2dif2  11661  recan  11663  cau3lem  11668  amgm2  11672  bdtrilem  11793  xrmaxadd  11815  xrbdtri  11830  climaddc1  11883  climsubc1  11886  climcvg1nlem  11903  serf0  11906  summodclem3  11934  summodclem2a  11935  summodc  11937  fsumsplitsn  11964  fsumm1  11970  fsumsplitsnun  11973  fsump1  11974  isummulc2  11980  fsumrev  11997  fisum0diag2  12001  fsummulc2  12002  fsumsub  12006  fsumabs  12019  telfsumo  12020  fsumparts  12024  fsumrelem  12025  fsumiun  12031  binomlem  12037  binom  12038  binom1p  12039  binom11  12040  binom1dif  12041  bcxmas  12043  isumsplit  12045  isum1p  12046  divcnv  12051  arisum2  12053  trireciplem  12054  trirecip  12055  geolim  12065  georeclim  12067  geo2sum  12068  geo2lim  12070  geoisum1c  12074  0.999...  12075  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  cvgratz  12086  mertenslem2  12090  mertensabs  12091  clim2prod  12093  prodfrecap  12100  prodfdivap  12101  prodmodclem3  12129  prodmodclem2a  12130  fprodm1  12152  fprodp1  12154  fprodunsn  12158  fprodfac  12169  fprodeq0  12171  fprodconst  12174  fprodrec  12183  fproddivap  12184  fprodsplitsn  12187  ege2le3  12225  efaddlem  12228  efsub  12235  efexp  12236  eftlub  12244  efsep  12245  effsumlt  12246  ef4p  12248  tanval3ap  12268  resinval  12269  recosval  12270  efi4p  12271  efival  12286  efmival  12287  efeul  12288  sinadd  12290  cosadd  12291  tanaddap  12293  sinsub  12294  cossub  12295  sincossq  12302  sin2t  12303  cos2t  12304  cos2tsin  12305  ef01bndlem  12310  sin01bnd  12311  cos01bnd  12312  cos12dec  12322  absef  12324  absefib  12325  efieq1re  12326  demoivreALT  12328  eirraplem  12331  dvdsexp  12415  oexpneg  12431  opeo  12451  omeo  12452  m1exp1  12455  flodddiv4  12490  flodddiv4t2lthalf  12493  bitsval  12497  bitsp1  12505  bitsinv1lem  12515  bitsinv1  12516  divgcdnnr  12540  gcdaddm  12548  gcdadd  12549  gcdid  12550  modgcd  12555  gcdmultipled  12557  dvdsgcdidd  12558  bezoutlemnewy  12560  bezoutlema  12563  bezoutlemb  12564  bezoutlemex  12565  bezoutlembz  12568  absmulgcd  12581  gcdmultiple  12584  gcdmultiplez  12585  rpmulgcd  12590  rplpwr  12591  eucalginv  12621  eucalg  12624  lcmneg  12639  lcmgcdlem  12642  lcmgcd  12643  lcmid  12645  lcm1  12646  mulgcddvds  12659  qredeq  12661  divgcdcoprmex  12667  prmind2  12685  rpexp1i  12719  pw2dvdslemn  12730  pw2dvdseulemle  12732  pw2dvdseu  12733  oddpwdclemxy  12734  oddpwdclemdvds  12735  oddpwdclemndvds  12736  oddpwdclemdc  12738  2sqpwodd  12741  nn0gcdsq  12765  phiprmpw  12787  eulerthlemrprm  12794  eulerthlema  12795  eulerthlemh  12796  eulerthlemth  12797  fermltl  12799  prmdiv  12800  hashgcdlem  12803  odzdvds  12811  vfermltl  12817  modprm0  12820  nnnn0modprm0  12821  modprmn0modprm0  12822  coprimeprodsq  12823  pythagtriplem1  12831  pythagtriplem4  12834  pythagtriplem12  12841  pythagtriplem14  12843  pythagtriplem16  12845  pythagtriplem18  12847  pythagtrip  12849  pcpremul  12859  pceu  12861  pczpre  12863  pcdiv  12868  pcqmul  12869  pcqdiv  12873  pcexp  12875  pcxqcl  12878  pczdvds  12880  pczndvds  12882  pczndvds2  12884  pcid  12890  pcneg  12891  pcdvdstr  12893  pcgcd1  12894  pcgcd  12895  pc2dvds  12896  pcaddlem  12905  pcadd  12906  pcadd2  12907  pcmpt  12909  pcmpt2  12910  fldivp1  12914  pcfac  12916  pcbc  12917  expnprm  12919  prmpwdvds  12921  pockthlem  12922  pockthi  12924  4sqlem7  12950  4sqlem9  12952  4sqlem10  12953  4sqlem2  12955  4sqlem3  12956  4sqlem4  12958  mul4sqlem  12959  4sqlem11  12967  4sqlem16  12972  4sqlem17  12973  4sqlem19  12975  setscomd  13116  ressvalsets  13140  strressid  13147  ressval3d  13148  ressinbasd  13150  ressressg  13151  ressabsg  13152  grpinvalem  13461  grpinva  13462  grprida  13463  isnsgrp  13482  sgrpass  13484  sgrp1  13487  sgrppropd  13489  prdssgrpd  13491  mnd32g  13503  mnd4g  13505  mndpropd  13516  prdsidlem  13523  prdsmndd  13524  imasmnd2  13528  mhmex  13538  mhmlin  13543  gsumwmhm  13574  grprcan  13613  grpsubval  13622  grpinvid2  13629  grpasscan2  13640  grpsubinv  13649  grpinvadd  13654  grpsubid1  13661  grpsubadd0sub  13663  grpsubadd  13664  grpsubsub  13665  grpaddsubass  13666  grppncan  13667  grpnnncan2  13673  grpsubpropd2  13681  imasgrp2  13690  mhmlem  13694  mhmid  13695  mhmmnd  13696  ghmgrp  13698  mulgnn0gsum  13708  mulgnnp1  13710  mulgaddcomlem  13725  mulgaddcom  13726  mulginvinv  13728  mulgnn0dir  13732  mulgdirlem  13733  mulgp1  13735  mulgneg2  13736  mulgnn0ass  13738  mulgass  13739  mulgmodid  13741  mulgsubdir  13742  nmzsubg  13790  0nsg  13794  eqger  13804  qussub  13817  ghmlin  13828  ghmsub  13831  conjghm  13856  ablsub4  13893  abladdsub4  13894  ablsubsub4  13899  ablsub32  13902  ablnnncan  13903  gsumfzmptfidmadd2  13920  gsumfzconst  13921  gsumfzmhm2  13924  gsumfzsnfd  13925  mgpress  13937  rngass  13945  rngdi  13946  rngdir  13947  rngrz  13952  rngmneg2  13954  rngsubdi  13957  rngsubdir  13958  rngpropd  13961  imasrng  13962  srgass  13977  srgpcomp  13996  srgpcompp  13997  srgpcomppsc  13998  srg1expzeq1  14001  ringpropd  14044  ringrz  14050  ringnegr  14058  ringmneg2  14060  ringsubdi  14062  ringsubdir  14063  ring1  14065  imasring  14070  opprrng  14083  opprring  14085  mulgass3  14091  dvdsrd  14101  unitgrp  14123  invrfvald  14129  dvr1  14145  dvrass  14146  dvrcan1  14147  dvrcan3  14148  rdivmuldivd  14151  subrginv  14244  subrgdv  14245  resrhm2b  14256  islmod  14298  lmodlema  14299  islmodd  14300  lmodvs0  14329  lmodvneg1  14337  lmodvsubval2  14349  lmodsubvs  14350  lmodsubdi  14351  lmodsubdir  14352  lmodprop2d  14355  rmodislmodlem  14357  rmodislmod  14358  lsssn0  14377  sraval  14444  cnfldsub  14582  gsumfzfsumlem0  14593  gsumfzfsumlemm  14594  mulgrhm  14616  mulgrhm2  14617  znval  14643  znval2  14645  znunit  14666  psrval  14673  mplvalcoe  14697  mplval2g  14702  restabs  14892  cnprcl2k  14923  cnrest2r  14954  ispsmet  15040  psmettri2  15045  psmetsym  15046  ismet  15061  isxmet  15062  xmettri2  15078  xmetsym  15085  xmettri3  15091  mettri3  15092  xblss2ps  15121  xblss2  15122  comet  15216  xmetxp  15224  xmetxpbl  15225  txmetcnp  15235  fsumcncntop  15284  cncfi  15295  divcncfap  15331  limccl  15376  ellimc3apf  15377  limccnpcntop  15392  limccnp2lem  15393  reldvg  15396  dvfvalap  15398  eldvap  15399  dvcj  15426  dvfre  15427  dvexp  15428  dvexp2  15429  dvrecap  15430  dvmptaddx  15436  dvmptmulx  15437  dvmptnegcn  15439  dvmptsubcn  15440  dvmptcjx  15441  dvmptfsum  15442  dveflem  15443  dvef  15444  plyconst  15462  plyaddlem1  15464  plymullem1  15465  plyadd  15468  plymul  15469  plycoeid3  15474  plycolemc  15475  plyco  15476  plycjlemc  15477  plycj  15478  plyrecj  15480  dvply1  15482  dvply2g  15483  sin0pilem1  15498  sin0pilem2  15499  efper  15524  sinperlem  15525  efimpi  15536  ptolemy  15541  tangtx  15555  abssinper  15563  cosq34lt1  15567  rpcxpef  15611  rpcxpp1  15623  rpcxpneg  15624  rpcxpsub  15625  rpmulcxp  15626  rpdivcxp  15628  cxpmul  15629  rpcxpmul2  15630  rpcxproot  15631  cxpcom  15655  rpabscxpbnd  15657  rplogbval  15662  rplogbreexp  15670  rplogbzexp  15671  rprelogbmulexp  15673  rprelogbdiv  15674  relogbexpap  15675  rplogbcxp  15680  rpcxplogb  15681  logbgcd1irr  15684  logbgcd1irraplemap  15686  binom4  15696  wilthlem1  15697  sgmval  15700  sgmppw  15709  1sgmprm  15711  mersenne  15714  perfectlem1  15716  perfectlem2  15717  perfect  15718  lgslem1  15722  lgsval  15726  lgsfvalg  15727  lgsval2lem  15732  lgsval4  15742  lgsneg  15746  lgsneg1  15747  lgsmod  15748  lgsdir2  15755  lgsdirprm  15756  lgsdilem2  15758  lgsdi  15759  lgsne0  15760  lgssq2  15763  lgsdirnn0  15769  lgsdinn0  15770  gausslemma2dlem1a  15780  gausslemma2dlem1f1o  15782  gausslemma2dlem2  15784  gausslemma2dlem3  15785  gausslemma2dlem4  15786  gausslemma2dlem5  15788  gausslemma2dlem6  15789  gausslemma2d  15791  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem3  15794  lgseisenlem4  15795  lgsquadlem1  15799  lgsquadlem2  15800  lgsquadlem3  15801  lgsquad2lem1  15803  lgsquad2lem2  15804  lgsquad2  15805  lgsquad3  15806  m1lgs  15807  2lgslem3c  15817  2lgslem3d  15818  2lgslem3d1  15822  2sqlem2  15837  2sqlem3  15839  2sqlem4  15840  2sqlem8  15845  2sqlem9  15846  2sqlem10  15847  vtxdumgrfival  16109  p1evtxdeqfi  16123  p1evtxdp1fi  16124  iswlk  16134  upgr2wlkdc  16186  wlkres  16188  trlreslem  16198  isclwwlk  16203  clwwlkccatlem  16209  clwwlknp  16226  clwwlkn1  16227  clwwlkn2  16230  clwwlkext2edg  16231  clwwlknonex2lem1  16246  clwwlknonex2lem2  16247  clwwlknonex2  16248  iseupth  16256  qdencn  16581  trilpolemclim  16590  trilpolemcl  16591  trilpolemisumle  16592  trilpolemeq1  16594  trilpolemlt1  16595  trilpo  16597  apdifflemf  16600  apdiff  16602  iswomni0  16605  redcwlpolemeq1  16608  redcwlpo  16609  nconstwlpolem0  16617  nconstwlpolemgt0  16618  nconstwlpo  16620  neapmkv  16622  gfsumval  16630  gsumgfsum1  16631  gsumgfsum  16634