Theorem oveq2d 5885

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 5877	. 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 1353  (class class class)co 5869

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2739  df-un 3133  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-iota 5174  df-fv 5220  df-ov 5872

This theorem is referenced by:  csbov1g  5909  caovassg  6027  caovdig  6043  caovdirg  6046  caov32d  6049  caov4d  6053  caov42d  6055  nnaass  6480  nndi  6481  nnmass  6482  nnmsucr  6483  ecovass  6638  ecoviass  6639  ecovdi  6640  ecovidi  6641  addasspig  7320  mulasspig  7322  distrpig  7323  dfplpq2  7344  mulpipq2  7361  addassnqg  7372  prarloclemarch  7408  prarloclemarch2  7409  ltrnqg  7410  enq0sym  7422  addnq0mo  7437  mulnq0mo  7438  addnnnq0  7439  nq0a0  7447  distrnq0  7449  addassnq0  7452  prarloclemlo  7484  prarloclem3  7487  prarloclem5  7490  prarloclemcalc  7492  addnqprl  7519  addnqpru  7520  prmuloclemcalc  7555  mulnqprl  7558  mulnqpru  7559  distrlem4prl  7574  distrlem4pru  7575  1idprl  7580  1idpru  7581  ltexprlemloc  7597  addcanprleml  7604  addcanprlemu  7605  recexprlem1ssu  7624  ltmprr  7632  caucvgprlemcanl  7634  cauappcvgprlemladdru  7646  cauappcvgprlemladdrl  7647  cauappcvgprlem1  7649  cauappcvgprlemlim  7651  caucvgprlemnkj  7656  caucvgprlemnbj  7657  caucvgprlemdisj  7664  caucvgprlemloc  7665  caucvgprlemcl  7666  caucvgprlemladdrl  7668  caucvgprlem1  7669  caucvgpr  7672  caucvgprprlemell  7675  caucvgprprlemcbv  7677  caucvgprprlemval  7678  caucvgprprlemnkeqj  7680  caucvgprprlemopl  7687  caucvgprprlemlol  7688  caucvgprprlemloc  7693  caucvgprprlemclphr  7695  caucvgprprlemexb  7697  caucvgprprlemaddq  7698  caucvgprprlem1  7699  addcmpblnr  7729  mulcmpblnrlemg  7730  addsrmo  7733  mulsrmo  7734  addsrpr  7735  mulsrpr  7736  ltsrprg  7737  recexgt0sr  7763  mulgt0sr  7768  caucvgsrlemgt1  7785  caucvgsrlemoffval  7786  caucvgsr  7792  suplocsrlemb  7796  suplocsrlempr  7797  suplocsrlem  7798  suplocsr  7799  mulcnsr  7825  pitoregt0  7839  recidpirqlemcalc  7847  axmulcom  7861  axmulass  7863  axdistr  7864  ax0id  7868  axcnre  7871  recriota  7880  axcaucvglemcau  7888  axcaucvglemres  7889  mulid1  7945  adddirp1d  7974  mul32  8077  mul31  8078  add32  8106  add4  8108  add42  8109  cnegex  8125  addcan2  8128  addsubass  8157  subsub2  8175  nppcan2  8178  sub32  8181  nnncan  8182  sub4  8192  muladd  8331  subdi  8332  mul2neg  8345  submul2  8346  mulsub  8348  mulsubfacd  8365  add20  8421  recexre  8525  rereim  8533  apreap  8534  ltmul1  8539  cru  8549  apreim  8550  mulreim  8551  apadd1  8555  apneg  8558  mulap0  8600  divrecap  8634  divassap  8636  divmulasscomap  8642  divsubdirap  8654  divdivdivap  8659  divmul24ap  8662  divmuleqap  8663  divcanap6  8665  divdivap1  8669  divdivap2  8670  divsubdivap  8674  conjmulap  8675  div2negap  8681  apmul1  8734  cju  8907  nnmulcl  8929  add1p1  9157  sub1m1  9158  cnm2m1cnm3  9159  xp1d2m1eqxm1d2  9160  div4p1lem1div2  9161  un0addcl  9198  un0mulcl  9199  zaddcllemneg  9281  qapne  9628  cnref1o  9639  rexsub  9840  xnegid  9846  xaddcom  9848  xnegdi  9855  xaddass  9856  xaddass2  9857  xpncan  9858  xnpcan  9859  xleadd1a  9860  xsubge0  9868  xposdif  9869  xlesubadd  9870  xadd4d  9872  lincmb01cmp  9990  iccf1o  9991  ige3m2fz  10035  fztp  10064  fzsuc2  10065  fseq1m1p1  10081  fzm1  10086  ige2m1fz1  10095  nn0split  10122  nnsplit  10123  fzval3  10190  zpnn0elfzo1  10194  fzosplitsnm1  10195  fzosplitprm1  10220  fzoshftral  10224  rebtwn2zlemstep  10239  flhalf  10288  modqval  10310  modqvalr  10311  modqdiffl  10321  modqfrac  10323  flqmod  10324  intqfrac  10325  zmod10  10326  modqmulnn  10328  modqvalp1  10329  modqid  10335  modqcyc  10345  modqcyc2  10346  modqmul1  10363  q2submod  10371  modqdi  10378  modqsubdir  10379  modqeqmodmin  10380  modsumfzodifsn  10382  addmodlteq  10384  frecuzrdgsuctlem  10409  uzsinds  10428  seqeq3  10436  iseqvalcbv  10443  seq3val  10444  seqvalcd  10445  seqf  10447  seq3p1  10448  seqovcd  10449  seqp1cd  10452  seq3m1  10454  seq3fveq2  10455  seq3shft2  10459  monoord2  10463  ser3mono  10464  seq3split  10465  seq3caopr3  10467  seq3caopr2  10468  seq3caopr  10469  seq3id2  10495  seq3homo  10496  seq3z  10497  exp3vallem  10507  exp3val  10508  expp1  10513  expnegap0  10514  expineg2  10515  expn1ap0  10516  expm1t  10534  1exp  10535  expnegzap  10540  mulexpzap  10546  expadd  10548  expaddzaplem  10549  expaddzap  10550  expmul  10551  expmulzap  10552  m1expeven  10553  expsubap  10554  expp1zap  10555  expm1ap  10556  expdivap  10557  iexpcyc  10610  subsq2  10613  binom2  10617  binom21  10618  binom2sub  10619  binom2sub1  10620  mulbinom2  10622  binom3  10623  zesq  10624  bernneq  10626  sqoddm1div8  10659  nn0opthlem1d  10684  nn0opthd  10686  facp1  10694  facnn2  10698  faclbnd  10705  faclbnd6  10708  bcval  10713  bccmpl  10718  bcn0  10719  bcnn  10721  bcnp1n  10723  bcm1k  10724  bcp1n  10725  bcp1nk  10726  bcval5  10727  bcp1m1  10729  bcpasc  10730  bcn2m1  10733  bcn2p1  10734  omgadd  10766  hashunlem  10768  hashunsng  10771  hashdifsn  10783  hashxp  10790  zfz1isolemsplit  10802  zfz1isolem1  10804  zfz1iso  10805  seq3coll  10806  shftcan1  10827  shftcan2  10828  cjval  10838  cjth  10839  crre  10850  replim  10852  remim  10853  reim0b  10855  rereb  10856  mulreap  10857  cjreb  10859  recj  10860  reneg  10861  readd  10862  resub  10863  remullem  10864  imcj  10868  imneg  10869  imadd  10870  imsub  10871  cjcj  10876  cjadd  10877  ipcnval  10879  cjmulrcl  10880  cjneg  10883  addcj  10884  cjsub  10885  cnrecnv  10903  caucvgrelemcau  10973  cvg1nlemcau  10977  cvg1nlemres  10978  recvguniqlem  10987  resqrexlemover  11003  resqrexlemlo  11006  resqrexlemcalc1  11007  resqrexlemcalc3  11009  resqrexlemnm  11011  resqrexlemcvg  11012  absneg  11043  abscj  11045  sqabsadd  11048  sqabssub  11049  absmul  11062  absid  11064  absre  11070  absresq  11071  absexpzap  11073  recvalap  11090  abstri  11097  abs2dif2  11100  recan  11102  cau3lem  11107  amgm2  11111  bdtrilem  11231  xrmaxadd  11253  xrbdtri  11268  climaddc1  11321  climsubc1  11324  climcvg1nlem  11341  serf0  11344  summodclem3  11372  summodclem2a  11373  summodc  11375  fsumsplitsn  11402  fsumm1  11408  fsumsplitsnun  11411  fsump1  11412  isummulc2  11418  fsumrev  11435  fisum0diag2  11439  fsummulc2  11440  fsumsub  11444  fsumabs  11457  telfsumo  11458  fsumparts  11462  fsumrelem  11463  fsumiun  11469  binomlem  11475  binom  11476  binom1p  11477  binom11  11478  binom1dif  11479  bcxmas  11481  isumsplit  11483  isum1p  11484  divcnv  11489  arisum2  11491  trireciplem  11492  trirecip  11493  geolim  11503  georeclim  11505  geo2sum  11506  geo2lim  11508  geoisum1c  11512  0.999...  11513  cvgratnnlemnexp  11516  cvgratnnlemmn  11517  cvgratz  11524  mertenslem2  11528  mertensabs  11529  clim2prod  11531  prodfrecap  11538  prodfdivap  11539  prodmodclem3  11567  prodmodclem2a  11568  fprodm1  11590  fprodp1  11592  fprodunsn  11596  fprodfac  11607  fprodeq0  11609  fprodconst  11612  fprodrec  11621  fproddivap  11622  fprodsplitsn  11625  ege2le3  11663  efaddlem  11666  efsub  11673  efexp  11674  eftlub  11682  efsep  11683  effsumlt  11684  ef4p  11686  tanval3ap  11706  resinval  11707  recosval  11708  efi4p  11709  efival  11724  efmival  11725  efeul  11726  sinadd  11728  cosadd  11729  tanaddap  11731  sinsub  11732  cossub  11733  sincossq  11740  sin2t  11741  cos2t  11742  cos2tsin  11743  ef01bndlem  11748  sin01bnd  11749  cos01bnd  11750  cos12dec  11759  absef  11761  absefib  11762  efieq1re  11763  demoivreALT  11765  eirraplem  11768  dvdsexp  11850  oexpneg  11865  opeo  11885  omeo  11886  m1exp1  11889  flodddiv4  11922  flodddiv4t2lthalf  11925  divgcdnnr  11960  gcdaddm  11968  gcdadd  11969  gcdid  11970  modgcd  11975  gcdmultipled  11977  dvdsgcdidd  11978  bezoutlemnewy  11980  bezoutlema  11983  bezoutlemb  11984  bezoutlemex  11985  bezoutlembz  11988  absmulgcd  12001  gcdmultiple  12004  gcdmultiplez  12005  rpmulgcd  12010  rplpwr  12011  eucalginv  12039  eucalg  12042  lcmneg  12057  lcmgcdlem  12060  lcmgcd  12061  lcmid  12063  lcm1  12064  mulgcddvds  12077  qredeq  12079  divgcdcoprmex  12085  prmind2  12103  rpexp1i  12137  pw2dvdslemn  12148  pw2dvdseulemle  12150  pw2dvdseu  12151  oddpwdclemxy  12152  oddpwdclemdvds  12153  oddpwdclemndvds  12154  oddpwdclemdc  12156  2sqpwodd  12159  nn0gcdsq  12183  phiprmpw  12205  eulerthlemrprm  12212  eulerthlema  12213  eulerthlemh  12214  eulerthlemth  12215  fermltl  12217  prmdiv  12218  hashgcdlem  12221  odzdvds  12228  vfermltl  12234  modprm0  12237  nnnn0modprm0  12238  modprmn0modprm0  12239  coprimeprodsq  12240  pythagtriplem1  12248  pythagtriplem4  12251  pythagtriplem12  12258  pythagtriplem14  12260  pythagtriplem16  12262  pythagtriplem18  12264  pythagtrip  12266  pcpremul  12276  pceu  12278  pczpre  12280  pcdiv  12285  pcqmul  12286  pcqdiv  12290  pcexp  12292  pczdvds  12296  pczndvds  12298  pczndvds2  12300  pcid  12306  pcneg  12307  pcdvdstr  12309  pcgcd1  12310  pcgcd  12311  pc2dvds  12312  pcaddlem  12321  pcadd  12322  pcmpt  12324  pcmpt2  12325  fldivp1  12329  pcfac  12331  pcbc  12332  expnprm  12334  prmpwdvds  12336  pockthlem  12337  pockthi  12339  4sqlem7  12365  4sqlem9  12367  4sqlem10  12368  4sqlem2  12370  4sqlem3  12371  4sqlem4  12373  mul4sqlem  12374  ressvalsets  12506  strressid  12512  ressval3d  12513  ressinbasd  12515  ressressg  12516  ressabsg  12517  grprinvlem  12696  grprinvd  12697  grpridd  12698  isnsgrp  12704  sgrpass  12706  sgrp1  12708  mnd32g  12720  mnd4g  12722  mndpropd  12733  mhmlin  12748  grprcan  12800  grpsubval  12809  grpinvid2  12815  grpasscan2  12823  grpsubinv  12832  grpinvadd  12837  grpsubid1  12844  grpsubadd0sub  12846  grpsubadd  12847  grpsubsub  12848  grpaddsubass  12849  grppncan  12850  grpnnncan2  12856  grpsubpropd2  12864  mhmlem  12867  mhmid  12868  mhmmnd  12869  ghmgrp  12871  mulgnnp1  12880  mulgaddcomlem  12894  mulgaddcom  12895  mulginvinv  12897  mulgnn0dir  12901  mulgdirlem  12902  mulgp1  12904  mulgneg2  12905  mulgnn0ass  12907  mulgass  12908  mulgmodid  12910  mulgsubdir  12911  ablsub4  12943  abladdsub4  12944  ablsubsub4  12949  ablsub32  12952  ablnnncan  12953  srgass  12980  srgpcomp  12999  srgpcompp  13000  srgpcomppsc  13001  srg1expzeq1  13004  ringpropd  13043  ringrz  13049  rngnegr  13055  ringmneg2  13057  ringsubdi  13059  rngsubdir  13060  ring1  13062  opprring  13074  mulgass3  13079  dvdsrd  13088  unitgrp  13110  invrfvald  13116  dvr1  13132  dvrass  13133  dvrcan1  13134  dvrcan3  13135  restabs  13342  cnprcl2k  13373  cnrest2r  13404  ispsmet  13490  psmettri2  13495  psmetsym  13496  ismet  13511  isxmet  13512  xmettri2  13528  xmetsym  13535  xmettri3  13541  mettri3  13542  xblss2ps  13571  xblss2  13572  comet  13666  xmetxp  13674  xmetxpbl  13675  txmetcnp  13685  fsumcncntop  13723  cncfi  13732  limccl  13795  ellimc3apf  13796  limccnpcntop  13811  limccnp2lem  13812  reldvg  13815  dvfvalap  13817  eldvap  13818  dvcj  13840  dvfre  13841  dvexp  13842  dvexp2  13843  dvrecap  13844  dvmptaddx  13848  dvmptmulx  13849  dvmptnegcn  13851  dvmptsubcn  13852  dvmptcjx  13853  dveflem  13854  dvef  13855  sin0pilem1  13869  sin0pilem2  13870  efper  13895  sinperlem  13896  efimpi  13907  ptolemy  13912  tangtx  13926  abssinper  13934  cosq34lt1  13938  rpcxpef  13982  rpcxpp1  13994  rpcxpneg  13995  rpcxpsub  13996  rpmulcxp  13997  rpdivcxp  13999  cxpmul  14000  rpcxproot  14001  cxpcom  14024  rpabscxpbnd  14026  rplogbval  14030  rplogbreexp  14038  rplogbzexp  14039  rprelogbmulexp  14041  rprelogbdiv  14042  relogbexpap  14043  rplogbcxp  14048  rpcxplogb  14049  logbgcd1irr  14052  logbgcd1irraplemap  14054  binom4  14064  lgslem1  14068  lgsval  14072  lgsfvalg  14073  lgsval2lem  14078  lgsval4  14088  lgsneg  14092  lgsneg1  14093  lgsmod  14094  lgsdir2  14101  lgsdirprm  14102  lgsdilem2  14104  lgsdi  14105  lgsne0  14106  lgssq2  14109  lgsdirnn0  14115  lgsdinn0  14116  2sqlem2  14118  2sqlem3  14120  2sqlem4  14121  2sqlem8  14126  2sqlem9  14127  2sqlem10  14128  qdencn  14431  trilpolemclim  14440  trilpolemcl  14441  trilpolemisumle  14442  trilpolemeq1  14444  trilpolemlt1  14445  trilpo  14447  apdifflemf  14450  apdiff  14452  iswomni0  14455  redcwlpolemeq1  14458  redcwlpo  14459  nconstwlpolem0  14466  nconstwlpolemgt0  14467  nconstwlpo  14469  neapmkv  14471