Theorem oveq2d 5912

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 5904	. 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 1364  (class class class)co 5896

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5196  df-fv 5243  df-ov 5899

This theorem is referenced by:  csbov1g  5936  caovassg  6055  caovdig  6071  caovdirg  6074  caov32d  6077  caov4d  6081  caov42d  6083  nnaass  6510  nndi  6511  nnmass  6512  nnmsucr  6513  ecovass  6670  ecoviass  6671  ecovdi  6672  ecovidi  6673  addasspig  7359  mulasspig  7361  distrpig  7362  dfplpq2  7383  mulpipq2  7400  addassnqg  7411  prarloclemarch  7447  prarloclemarch2  7448  ltrnqg  7449  enq0sym  7461  addnq0mo  7476  mulnq0mo  7477  addnnnq0  7478  nq0a0  7486  distrnq0  7488  addassnq0  7491  prarloclemlo  7523  prarloclem3  7526  prarloclem5  7529  prarloclemcalc  7531  addnqprl  7558  addnqpru  7559  prmuloclemcalc  7594  mulnqprl  7597  mulnqpru  7598  distrlem4prl  7613  distrlem4pru  7614  1idprl  7619  1idpru  7620  ltexprlemloc  7636  addcanprleml  7643  addcanprlemu  7644  recexprlem1ssu  7663  ltmprr  7671  caucvgprlemcanl  7673  cauappcvgprlemladdru  7685  cauappcvgprlemladdrl  7686  cauappcvgprlem1  7688  cauappcvgprlemlim  7690  caucvgprlemnkj  7695  caucvgprlemnbj  7696  caucvgprlemdisj  7703  caucvgprlemloc  7704  caucvgprlemcl  7705  caucvgprlemladdrl  7707  caucvgprlem1  7708  caucvgpr  7711  caucvgprprlemell  7714  caucvgprprlemcbv  7716  caucvgprprlemval  7717  caucvgprprlemnkeqj  7719  caucvgprprlemopl  7726  caucvgprprlemlol  7727  caucvgprprlemloc  7732  caucvgprprlemclphr  7734  caucvgprprlemexb  7736  caucvgprprlemaddq  7737  caucvgprprlem1  7738  addcmpblnr  7768  mulcmpblnrlemg  7769  addsrmo  7772  mulsrmo  7773  addsrpr  7774  mulsrpr  7775  ltsrprg  7776  recexgt0sr  7802  mulgt0sr  7807  caucvgsrlemgt1  7824  caucvgsrlemoffval  7825  caucvgsr  7831  suplocsrlemb  7835  suplocsrlempr  7836  suplocsrlem  7837  suplocsr  7838  mulcnsr  7864  pitoregt0  7878  recidpirqlemcalc  7886  axmulcom  7900  axmulass  7902  axdistr  7903  ax0id  7907  axcnre  7910  recriota  7919  axcaucvglemcau  7927  axcaucvglemres  7928  mulrid  7984  adddirp1d  8014  mul32  8117  mul31  8118  add32  8146  add4  8148  add42  8149  cnegex  8165  addcan2  8168  addsubass  8197  subsub2  8215  nppcan2  8218  sub32  8221  nnncan  8222  sub4  8232  muladd  8371  subdi  8372  mul2neg  8385  submul2  8386  mulsub  8388  mulsubfacd  8405  add20  8461  recexre  8565  rereim  8573  apreap  8574  ltmul1  8579  cru  8589  apreim  8590  mulreim  8591  apadd1  8595  apneg  8598  mulap0  8641  divrecap  8675  divassap  8677  divmulasscomap  8683  divsubdirap  8695  divdivdivap  8700  divmul24ap  8703  divmuleqap  8704  divcanap6  8706  divdivap1  8710  divdivap2  8711  divsubdivap  8715  conjmulap  8716  div2negap  8722  apmul1  8775  cju  8948  nnmulcl  8970  add1p1  9198  sub1m1  9199  cnm2m1cnm3  9200  xp1d2m1eqxm1d2  9201  div4p1lem1div2  9202  un0addcl  9239  un0mulcl  9240  zaddcllemneg  9322  qapne  9669  cnref1o  9680  rexsub  9883  xnegid  9889  xaddcom  9891  xnegdi  9898  xaddass  9899  xaddass2  9900  xpncan  9901  xnpcan  9902  xleadd1a  9903  xsubge0  9911  xposdif  9912  xlesubadd  9913  xadd4d  9915  lincmb01cmp  10033  iccf1o  10034  ige3m2fz  10079  fztp  10108  fzsuc2  10109  fseq1m1p1  10125  fzm1  10130  ige2m1fz1  10139  nn0split  10166  nnsplit  10167  fzval3  10234  zpnn0elfzo1  10238  fzosplitsnm1  10239  fzosplitprm1  10264  fzoshftral  10268  rebtwn2zlemstep  10283  flhalf  10333  modqval  10355  modqvalr  10356  modqdiffl  10366  modqfrac  10368  flqmod  10369  intqfrac  10370  zmod10  10371  modqmulnn  10373  modqvalp1  10374  modqid  10380  modqcyc  10390  modqcyc2  10391  modqmul1  10408  q2submod  10416  modqdi  10423  modqsubdir  10424  modqeqmodmin  10425  modsumfzodifsn  10427  addmodlteq  10429  frecuzrdgsuctlem  10454  uzsinds  10473  seqeq3  10481  iseqvalcbv  10488  seq3val  10489  seqvalcd  10490  seqf  10492  seq3p1  10493  seqovcd  10494  seqp1cd  10497  seq3m1  10499  seq3fveq2  10500  seq3shft2  10504  monoord2  10508  ser3mono  10509  seq3split  10510  seq3caopr3  10512  seq3caopr2  10513  seq3caopr  10514  seq3id2  10540  seq3homo  10541  seq3z  10542  exp3vallem  10552  exp3val  10553  expp1  10558  expnegap0  10559  expineg2  10560  expn1ap0  10561  expm1t  10579  1exp  10580  expnegzap  10585  mulexpzap  10591  expadd  10593  expaddzaplem  10594  expaddzap  10595  expmul  10596  expmulzap  10597  m1expeven  10598  expsubap  10599  expp1zap  10600  expm1ap  10601  expdivap  10602  iexpcyc  10656  subsq2  10659  binom2  10663  binom21  10664  binom2sub  10665  binom2sub1  10666  mulbinom2  10668  binom3  10669  zesq  10670  bernneq  10672  sqoddm1div8  10705  mulsubdivbinom2ap  10723  nn0opthlem1d  10732  nn0opthd  10734  facp1  10742  facnn2  10746  faclbnd  10753  faclbnd6  10756  bcval  10761  bccmpl  10766  bcn0  10767  bcnn  10769  bcnp1n  10771  bcm1k  10772  bcp1n  10773  bcp1nk  10774  bcval5  10775  bcp1m1  10777  bcpasc  10778  bcn2m1  10781  bcn2p1  10782  omgadd  10814  hashunlem  10816  hashunsng  10819  hashdifsn  10831  hashxp  10838  zfz1isolemsplit  10850  zfz1isolem1  10852  zfz1iso  10853  seq3coll  10854  shftcan1  10875  shftcan2  10876  cjval  10886  cjth  10887  crre  10898  replim  10900  remim  10901  reim0b  10903  rereb  10904  mulreap  10905  cjreb  10907  recj  10908  reneg  10909  readd  10910  resub  10911  remullem  10912  imcj  10916  imneg  10917  imadd  10918  imsub  10919  cjcj  10924  cjadd  10925  ipcnval  10927  cjmulrcl  10928  cjneg  10931  addcj  10932  cjsub  10933  cnrecnv  10951  caucvgrelemcau  11021  cvg1nlemcau  11025  cvg1nlemres  11026  recvguniqlem  11035  resqrexlemover  11051  resqrexlemlo  11054  resqrexlemcalc1  11055  resqrexlemcalc3  11057  resqrexlemnm  11059  resqrexlemcvg  11060  absneg  11091  abscj  11093  sqabsadd  11096  sqabssub  11097  absmul  11110  absid  11112  absre  11118  absresq  11119  absexpzap  11121  recvalap  11138  abstri  11145  abs2dif2  11148  recan  11150  cau3lem  11155  amgm2  11159  bdtrilem  11279  xrmaxadd  11301  xrbdtri  11316  climaddc1  11369  climsubc1  11372  climcvg1nlem  11389  serf0  11392  summodclem3  11420  summodclem2a  11421  summodc  11423  fsumsplitsn  11450  fsumm1  11456  fsumsplitsnun  11459  fsump1  11460  isummulc2  11466  fsumrev  11483  fisum0diag2  11487  fsummulc2  11488  fsumsub  11492  fsumabs  11505  telfsumo  11506  fsumparts  11510  fsumrelem  11511  fsumiun  11517  binomlem  11523  binom  11524  binom1p  11525  binom11  11526  binom1dif  11527  bcxmas  11529  isumsplit  11531  isum1p  11532  divcnv  11537  arisum2  11539  trireciplem  11540  trirecip  11541  geolim  11551  georeclim  11553  geo2sum  11554  geo2lim  11556  geoisum1c  11560  0.999...  11561  cvgratnnlemnexp  11564  cvgratnnlemmn  11565  cvgratz  11572  mertenslem2  11576  mertensabs  11577  clim2prod  11579  prodfrecap  11586  prodfdivap  11587  prodmodclem3  11615  prodmodclem2a  11616  fprodm1  11638  fprodp1  11640  fprodunsn  11644  fprodfac  11655  fprodeq0  11657  fprodconst  11660  fprodrec  11669  fproddivap  11670  fprodsplitsn  11673  ege2le3  11711  efaddlem  11714  efsub  11721  efexp  11722  eftlub  11730  efsep  11731  effsumlt  11732  ef4p  11734  tanval3ap  11754  resinval  11755  recosval  11756  efi4p  11757  efival  11772  efmival  11773  efeul  11774  sinadd  11776  cosadd  11777  tanaddap  11779  sinsub  11780  cossub  11781  sincossq  11788  sin2t  11789  cos2t  11790  cos2tsin  11791  ef01bndlem  11796  sin01bnd  11797  cos01bnd  11798  cos12dec  11807  absef  11809  absefib  11810  efieq1re  11811  demoivreALT  11813  eirraplem  11816  dvdsexp  11899  oexpneg  11914  opeo  11934  omeo  11935  m1exp1  11938  flodddiv4  11971  flodddiv4t2lthalf  11974  divgcdnnr  12009  gcdaddm  12017  gcdadd  12018  gcdid  12019  modgcd  12024  gcdmultipled  12026  dvdsgcdidd  12027  bezoutlemnewy  12029  bezoutlema  12032  bezoutlemb  12033  bezoutlemex  12034  bezoutlembz  12037  absmulgcd  12050  gcdmultiple  12053  gcdmultiplez  12054  rpmulgcd  12059  rplpwr  12060  eucalginv  12088  eucalg  12091  lcmneg  12106  lcmgcdlem  12109  lcmgcd  12110  lcmid  12112  lcm1  12113  mulgcddvds  12126  qredeq  12128  divgcdcoprmex  12134  prmind2  12152  rpexp1i  12186  pw2dvdslemn  12197  pw2dvdseulemle  12199  pw2dvdseu  12200  oddpwdclemxy  12201  oddpwdclemdvds  12202  oddpwdclemndvds  12203  oddpwdclemdc  12205  2sqpwodd  12208  nn0gcdsq  12232  phiprmpw  12254  eulerthlemrprm  12261  eulerthlema  12262  eulerthlemh  12263  eulerthlemth  12264  fermltl  12266  prmdiv  12267  hashgcdlem  12270  odzdvds  12277  vfermltl  12283  modprm0  12286  nnnn0modprm0  12287  modprmn0modprm0  12288  coprimeprodsq  12289  pythagtriplem1  12297  pythagtriplem4  12300  pythagtriplem12  12307  pythagtriplem14  12309  pythagtriplem16  12311  pythagtriplem18  12313  pythagtrip  12315  pcpremul  12325  pceu  12327  pczpre  12329  pcdiv  12334  pcqmul  12335  pcqdiv  12339  pcexp  12341  pcxqcl  12344  pczdvds  12346  pczndvds  12348  pczndvds2  12350  pcid  12356  pcneg  12357  pcdvdstr  12359  pcgcd1  12360  pcgcd  12361  pc2dvds  12362  pcaddlem  12371  pcadd  12372  pcadd2  12373  pcmpt  12375  pcmpt2  12376  fldivp1  12380  pcfac  12382  pcbc  12383  expnprm  12385  prmpwdvds  12387  pockthlem  12388  pockthi  12390  4sqlem7  12416  4sqlem9  12418  4sqlem10  12419  4sqlem2  12421  4sqlem3  12422  4sqlem4  12424  mul4sqlem  12425  4sqlem11  12433  4sqlem16  12438  4sqlem17  12439  4sqlem19  12441  setscomd  12553  ressvalsets  12576  strressid  12583  ressval3d  12584  ressinbasd  12586  ressressg  12587  ressabsg  12588  grpinvalem  12861  grpinva  12862  grprida  12863  isnsgrp  12869  sgrpass  12871  sgrp1  12874  sgrppropd  12876  mnd32g  12888  mnd4g  12890  mndpropd  12901  mhmex  12914  mhmlin  12919  grprcan  12981  grpsubval  12990  grpinvid2  12997  grpasscan2  13008  grpsubinv  13017  grpinvadd  13022  grpsubid1  13029  grpsubadd0sub  13031  grpsubadd  13032  grpsubsub  13033  grpaddsubass  13034  grppncan  13035  grpnnncan2  13041  grpsubpropd2  13049  imasgrp2  13052  mhmlem  13056  mhmid  13057  mhmmnd  13058  ghmgrp  13060  mulgnnp1  13070  mulgaddcomlem  13085  mulgaddcom  13086  mulginvinv  13088  mulgnn0dir  13092  mulgdirlem  13093  mulgp1  13095  mulgneg2  13096  mulgnn0ass  13098  mulgass  13099  mulgmodid  13101  mulgsubdir  13102  nmzsubg  13149  0nsg  13153  eqger  13163  qussub  13176  ghmlin  13187  ghmsub  13190  conjghm  13215  ablsub4  13252  abladdsub4  13253  ablsubsub4  13258  ablsub32  13261  ablnnncan  13262  mgpress  13285  rngass  13293  rngdi  13294  rngdir  13295  rngrz  13300  rngmneg2  13302  rngsubdi  13305  rngsubdir  13306  rngpropd  13309  imasrng  13310  srgass  13325  srgpcomp  13344  srgpcompp  13345  srgpcomppsc  13346  srg1expzeq1  13349  ringpropd  13392  ringrz  13398  ringnegr  13404  ringmneg2  13406  ringsubdi  13408  ringsubdir  13409  ring1  13411  imasring  13414  opprrng  13427  opprring  13429  mulgass3  13435  dvdsrd  13444  unitgrp  13466  invrfvald  13472  dvr1  13488  dvrass  13489  dvrcan1  13490  dvrcan3  13491  rdivmuldivd  13494  subrginv  13584  subrgdv  13585  islmod  13607  lmodlema  13608  islmodd  13609  lmodvs0  13638  lmodvneg1  13646  lmodvsubval2  13658  lmodsubvs  13659  lmodsubdi  13660  lmodsubdir  13661  lmodprop2d  13664  rmodislmodlem  13666  rmodislmod  13667  lsssn0  13686  sraval  13753  cnfldsub  13878  mulgrhm  13907  mulgrhm2  13908  znval  13932  znval2  13934  psrval  13944  restabs  14135  cnprcl2k  14166  cnrest2r  14197  ispsmet  14283  psmettri2  14288  psmetsym  14289  ismet  14304  isxmet  14305  xmettri2  14321  xmetsym  14328  xmettri3  14334  mettri3  14335  xblss2ps  14364  xblss2  14365  comet  14459  xmetxp  14467  xmetxpbl  14468  txmetcnp  14478  fsumcncntop  14516  cncfi  14525  limccl  14588  ellimc3apf  14589  limccnpcntop  14604  limccnp2lem  14605  reldvg  14608  dvfvalap  14610  eldvap  14611  dvcj  14633  dvfre  14634  dvexp  14635  dvexp2  14636  dvrecap  14637  dvmptaddx  14641  dvmptmulx  14642  dvmptnegcn  14644  dvmptsubcn  14645  dvmptcjx  14646  dveflem  14647  dvef  14648  sin0pilem1  14662  sin0pilem2  14663  efper  14688  sinperlem  14689  efimpi  14700  ptolemy  14705  tangtx  14719  abssinper  14727  cosq34lt1  14731  rpcxpef  14775  rpcxpp1  14787  rpcxpneg  14788  rpcxpsub  14789  rpmulcxp  14790  rpdivcxp  14792  cxpmul  14793  rpcxproot  14794  cxpcom  14817  rpabscxpbnd  14819  rplogbval  14823  rplogbreexp  14831  rplogbzexp  14832  rprelogbmulexp  14834  rprelogbdiv  14835  relogbexpap  14836  rplogbcxp  14841  rpcxplogb  14842  logbgcd1irr  14845  logbgcd1irraplemap  14847  binom4  14857  wilthlem1  14858  lgslem1  14862  lgsval  14866  lgsfvalg  14867  lgsval2lem  14872  lgsval4  14882  lgsneg  14886  lgsneg1  14887  lgsmod  14888  lgsdir2  14895  lgsdirprm  14896  lgsdilem2  14898  lgsdi  14899  lgsne0  14900  lgssq2  14903  lgsdirnn0  14909  lgsdinn0  14910  lgseisenlem1  14911  lgseisenlem2  14912  m1lgs  14913  2sqlem2  14923  2sqlem3  14925  2sqlem4  14926  2sqlem8  14931  2sqlem9  14932  2sqlem10  14933  qdencn  15237  trilpolemclim  15246  trilpolemcl  15247  trilpolemisumle  15248  trilpolemeq1  15250  trilpolemlt1  15251  trilpo  15253  apdifflemf  15256  apdiff  15258  iswomni0  15261  redcwlpolemeq1  15264  redcwlpo  15265  nconstwlpolem0  15273  nconstwlpolemgt0  15274  nconstwlpo  15276  neapmkv  15278