Theorem oveq2d 5858

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 5850	. 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 1343  (class class class)co 5842

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-3an 970  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2297  df-rex 2450  df-v 2728  df-un 3120  df-sn 3582  df-pr 3583  df-op 3585  df-uni 3790  df-br 3983  df-iota 5153  df-fv 5196  df-ov 5845

This theorem is referenced by:  csbov1g  5882  caovassg  6000  caovdig  6016  caovdirg  6019  caov32d  6022  caov4d  6026  caov42d  6028  nnaass  6453  nndi  6454  nnmass  6455  nnmsucr  6456  ecovass  6610  ecoviass  6611  ecovdi  6612  ecovidi  6613  addasspig  7271  mulasspig  7273  distrpig  7274  dfplpq2  7295  mulpipq2  7312  addassnqg  7323  prarloclemarch  7359  prarloclemarch2  7360  ltrnqg  7361  enq0sym  7373  addnq0mo  7388  mulnq0mo  7389  addnnnq0  7390  nq0a0  7398  distrnq0  7400  addassnq0  7403  prarloclemlo  7435  prarloclem3  7438  prarloclem5  7441  prarloclemcalc  7443  addnqprl  7470  addnqpru  7471  prmuloclemcalc  7506  mulnqprl  7509  mulnqpru  7510  distrlem4prl  7525  distrlem4pru  7526  1idprl  7531  1idpru  7532  ltexprlemloc  7548  addcanprleml  7555  addcanprlemu  7556  recexprlem1ssu  7575  ltmprr  7583  caucvgprlemcanl  7585  cauappcvgprlemladdru  7597  cauappcvgprlemladdrl  7598  cauappcvgprlem1  7600  cauappcvgprlemlim  7602  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemdisj  7615  caucvgprlemloc  7616  caucvgprlemcl  7617  caucvgprlemladdrl  7619  caucvgprlem1  7620  caucvgpr  7623  caucvgprprlemell  7626  caucvgprprlemcbv  7628  caucvgprprlemval  7629  caucvgprprlemnkeqj  7631  caucvgprprlemopl  7638  caucvgprprlemlol  7639  caucvgprprlemloc  7644  caucvgprprlemclphr  7646  caucvgprprlemexb  7648  caucvgprprlemaddq  7649  caucvgprprlem1  7650  addcmpblnr  7680  mulcmpblnrlemg  7681  addsrmo  7684  mulsrmo  7685  addsrpr  7686  mulsrpr  7687  ltsrprg  7688  recexgt0sr  7714  mulgt0sr  7719  caucvgsrlemgt1  7736  caucvgsrlemoffval  7737  caucvgsr  7743  suplocsrlemb  7747  suplocsrlempr  7748  suplocsrlem  7749  suplocsr  7750  mulcnsr  7776  pitoregt0  7790  recidpirqlemcalc  7798  axmulcom  7812  axmulass  7814  axdistr  7815  ax0id  7819  axcnre  7822  recriota  7831  axcaucvglemcau  7839  axcaucvglemres  7840  mulid1  7896  adddirp1d  7925  mul32  8028  mul31  8029  add32  8057  add4  8059  add42  8060  cnegex  8076  addcan2  8079  addsubass  8108  subsub2  8126  nppcan2  8129  sub32  8132  nnncan  8133  sub4  8143  muladd  8282  subdi  8283  mul2neg  8296  submul2  8297  mulsub  8299  mulsubfacd  8316  add20  8372  recexre  8476  rereim  8484  apreap  8485  ltmul1  8490  cru  8500  apreim  8501  mulreim  8502  apadd1  8506  apneg  8509  mulap0  8551  divrecap  8584  divassap  8586  divmulasscomap  8592  divsubdirap  8604  divdivdivap  8609  divmul24ap  8612  divmuleqap  8613  divcanap6  8615  divdivap1  8619  divdivap2  8620  divsubdivap  8624  conjmulap  8625  div2negap  8631  apmul1  8684  cju  8856  nnmulcl  8878  add1p1  9106  sub1m1  9107  cnm2m1cnm3  9108  xp1d2m1eqxm1d2  9109  div4p1lem1div2  9110  un0addcl  9147  un0mulcl  9148  zaddcllemneg  9230  qapne  9577  cnref1o  9588  rexsub  9789  xnegid  9795  xaddcom  9797  xnegdi  9804  xaddass  9805  xaddass2  9806  xpncan  9807  xnpcan  9808  xleadd1a  9809  xsubge0  9817  xposdif  9818  xlesubadd  9819  xadd4d  9821  lincmb01cmp  9939  iccf1o  9940  ige3m2fz  9984  fztp  10013  fzsuc2  10014  fseq1m1p1  10030  fzm1  10035  ige2m1fz1  10044  nn0split  10071  nnsplit  10072  fzval3  10139  zpnn0elfzo1  10143  fzosplitsnm1  10144  fzosplitprm1  10169  fzoshftral  10173  rebtwn2zlemstep  10188  flhalf  10237  modqval  10259  modqvalr  10260  modqdiffl  10270  modqfrac  10272  flqmod  10273  intqfrac  10274  zmod10  10275  modqmulnn  10277  modqvalp1  10278  modqid  10284  modqcyc  10294  modqcyc2  10295  modqmul1  10312  q2submod  10320  modqdi  10327  modqsubdir  10328  modqeqmodmin  10329  modsumfzodifsn  10331  addmodlteq  10333  frecuzrdgsuctlem  10358  uzsinds  10377  seqeq3  10385  iseqvalcbv  10392  seq3val  10393  seqvalcd  10394  seqf  10396  seq3p1  10397  seqovcd  10398  seqp1cd  10401  seq3m1  10403  seq3fveq2  10404  seq3shft2  10408  monoord2  10412  ser3mono  10413  seq3split  10414  seq3caopr3  10416  seq3caopr2  10417  seq3caopr  10418  seq3id2  10444  seq3homo  10445  seq3z  10446  exp3vallem  10456  exp3val  10457  expp1  10462  expnegap0  10463  expineg2  10464  expn1ap0  10465  expm1t  10483  1exp  10484  expnegzap  10489  mulexpzap  10495  expadd  10497  expaddzaplem  10498  expaddzap  10499  expmul  10500  expmulzap  10501  m1expeven  10502  expsubap  10503  expp1zap  10504  expm1ap  10505  expdivap  10506  iexpcyc  10559  subsq2  10562  binom2  10566  binom21  10567  binom2sub  10568  binom2sub1  10569  mulbinom2  10571  binom3  10572  zesq  10573  bernneq  10575  sqoddm1div8  10608  nn0opthlem1d  10633  nn0opthd  10635  facp1  10643  facnn2  10647  faclbnd  10654  faclbnd6  10657  bcval  10662  bccmpl  10667  bcn0  10668  bcnn  10670  bcnp1n  10672  bcm1k  10673  bcp1n  10674  bcp1nk  10675  bcval5  10676  bcp1m1  10678  bcpasc  10679  bcn2m1  10682  bcn2p1  10683  omgadd  10715  hashunlem  10717  hashunsng  10720  hashdifsn  10732  hashxp  10739  zfz1isolemsplit  10751  zfz1isolem1  10753  zfz1iso  10754  seq3coll  10755  shftcan1  10776  shftcan2  10777  cjval  10787  cjth  10788  crre  10799  replim  10801  remim  10802  reim0b  10804  rereb  10805  mulreap  10806  cjreb  10808  recj  10809  reneg  10810  readd  10811  resub  10812  remullem  10813  imcj  10817  imneg  10818  imadd  10819  imsub  10820  cjcj  10825  cjadd  10826  ipcnval  10828  cjmulrcl  10829  cjneg  10832  addcj  10833  cjsub  10834  cnrecnv  10852  caucvgrelemcau  10922  cvg1nlemcau  10926  cvg1nlemres  10927  recvguniqlem  10936  resqrexlemover  10952  resqrexlemlo  10955  resqrexlemcalc1  10956  resqrexlemcalc3  10958  resqrexlemnm  10960  resqrexlemcvg  10961  absneg  10992  abscj  10994  sqabsadd  10997  sqabssub  10998  absmul  11011  absid  11013  absre  11019  absresq  11020  absexpzap  11022  recvalap  11039  abstri  11046  abs2dif2  11049  recan  11051  cau3lem  11056  amgm2  11060  bdtrilem  11180  xrmaxadd  11202  xrbdtri  11217  climaddc1  11270  climsubc1  11273  climcvg1nlem  11290  serf0  11293  summodclem3  11321  summodclem2a  11322  summodc  11324  fsumsplitsn  11351  fsumm1  11357  fsumsplitsnun  11360  fsump1  11361  isummulc2  11367  fsumrev  11384  fisum0diag2  11388  fsummulc2  11389  fsumsub  11393  fsumabs  11406  telfsumo  11407  fsumparts  11411  fsumrelem  11412  fsumiun  11418  binomlem  11424  binom  11425  binom1p  11426  binom11  11427  binom1dif  11428  bcxmas  11430  isumsplit  11432  isum1p  11433  divcnv  11438  arisum2  11440  trireciplem  11441  trirecip  11442  geolim  11452  georeclim  11454  geo2sum  11455  geo2lim  11457  geoisum1c  11461  0.999...  11462  cvgratnnlemnexp  11465  cvgratnnlemmn  11466  cvgratz  11473  mertenslem2  11477  mertensabs  11478  clim2prod  11480  prodfrecap  11487  prodfdivap  11488  prodmodclem3  11516  prodmodclem2a  11517  fprodm1  11539  fprodp1  11541  fprodunsn  11545  fprodfac  11556  fprodeq0  11558  fprodconst  11561  fprodrec  11570  fproddivap  11571  fprodsplitsn  11574  ege2le3  11612  efaddlem  11615  efsub  11622  efexp  11623  eftlub  11631  efsep  11632  effsumlt  11633  ef4p  11635  tanval3ap  11655  resinval  11656  recosval  11657  efi4p  11658  efival  11673  efmival  11674  efeul  11675  sinadd  11677  cosadd  11678  tanaddap  11680  sinsub  11681  cossub  11682  sincossq  11689  sin2t  11690  cos2t  11691  cos2tsin  11692  ef01bndlem  11697  sin01bnd  11698  cos01bnd  11699  cos12dec  11708  absef  11710  absefib  11711  efieq1re  11712  demoivreALT  11714  eirraplem  11717  dvdsexp  11799  oexpneg  11814  opeo  11834  omeo  11835  m1exp1  11838  flodddiv4  11871  flodddiv4t2lthalf  11874  divgcdnnr  11909  gcdaddm  11917  gcdadd  11918  gcdid  11919  modgcd  11924  gcdmultipled  11926  dvdsgcdidd  11927  bezoutlemnewy  11929  bezoutlema  11932  bezoutlemb  11933  bezoutlemex  11934  bezoutlembz  11937  absmulgcd  11950  gcdmultiple  11953  gcdmultiplez  11954  rpmulgcd  11959  rplpwr  11960  eucalginv  11988  eucalg  11991  lcmneg  12006  lcmgcdlem  12009  lcmgcd  12010  lcmid  12012  lcm1  12013  mulgcddvds  12026  qredeq  12028  divgcdcoprmex  12034  prmind2  12052  rpexp1i  12086  pw2dvdslemn  12097  pw2dvdseulemle  12099  pw2dvdseu  12100  oddpwdclemxy  12101  oddpwdclemdvds  12102  oddpwdclemndvds  12103  oddpwdclemdc  12105  2sqpwodd  12108  nn0gcdsq  12132  phiprmpw  12154  eulerthlemrprm  12161  eulerthlema  12162  eulerthlemh  12163  eulerthlemth  12164  fermltl  12166  prmdiv  12167  hashgcdlem  12170  odzdvds  12177  vfermltl  12183  modprm0  12186  nnnn0modprm0  12187  modprmn0modprm0  12188  coprimeprodsq  12189  pythagtriplem1  12197  pythagtriplem4  12200  pythagtriplem12  12207  pythagtriplem14  12209  pythagtriplem16  12211  pythagtriplem18  12213  pythagtrip  12215  pcpremul  12225  pceu  12227  pczpre  12229  pcdiv  12234  pcqmul  12235  pcqdiv  12239  pcexp  12241  pczdvds  12245  pczndvds  12247  pczndvds2  12249  pcid  12255  pcneg  12256  pcdvdstr  12258  pcgcd1  12259  pcgcd  12260  pc2dvds  12261  pcaddlem  12270  pcadd  12271  pcmpt  12273  pcmpt2  12274  fldivp1  12278  pcfac  12280  pcbc  12281  expnprm  12283  prmpwdvds  12285  pockthlem  12286  pockthi  12288  4sqlem7  12314  4sqlem9  12316  4sqlem10  12317  4sqlem2  12319  4sqlem3  12320  4sqlem4  12322  mul4sqlem  12323  grprinvlem  12616  grprinvd  12617  grpridd  12618  restabs  12815  cnprcl2k  12846  cnrest2r  12877  ispsmet  12963  psmettri2  12968  psmetsym  12969  ismet  12984  isxmet  12985  xmettri2  13001  xmetsym  13008  xmettri3  13014  mettri3  13015  xblss2ps  13044  xblss2  13045  comet  13139  xmetxp  13147  xmetxpbl  13148  txmetcnp  13158  fsumcncntop  13196  cncfi  13205  limccl  13268  ellimc3apf  13269  limccnpcntop  13284  limccnp2lem  13285  reldvg  13288  dvfvalap  13290  eldvap  13291  dvcj  13313  dvfre  13314  dvexp  13315  dvexp2  13316  dvrecap  13317  dvmptaddx  13321  dvmptmulx  13322  dvmptnegcn  13324  dvmptsubcn  13325  dvmptcjx  13326  dveflem  13327  dvef  13328  sin0pilem1  13342  sin0pilem2  13343  efper  13368  sinperlem  13369  efimpi  13380  ptolemy  13385  tangtx  13399  abssinper  13407  cosq34lt1  13411  rpcxpef  13455  rpcxpp1  13467  rpcxpneg  13468  rpcxpsub  13469  rpmulcxp  13470  rpdivcxp  13472  cxpmul  13473  rpcxproot  13474  cxpcom  13497  rpabscxpbnd  13499  rplogbval  13503  rplogbreexp  13511  rplogbzexp  13512  rprelogbmulexp  13514  rprelogbdiv  13515  relogbexpap  13516  rplogbcxp  13521  rpcxplogb  13522  logbgcd1irr  13525  logbgcd1irraplemap  13527  binom4  13537  lgslem1  13541  lgsval  13545  lgsfvalg  13546  lgsval2lem  13551  lgsval4  13561  lgsneg  13565  lgsneg1  13566  lgsmod  13567  lgsdir2  13574  lgsdirprm  13575  lgsdilem2  13577  lgsdi  13578  lgsne0  13579  lgssq2  13582  lgsdirnn0  13588  lgsdinn0  13589  2sqlem2  13591  2sqlem3  13593  2sqlem4  13594  2sqlem8  13599  2sqlem9  13600  2sqlem10  13601  qdencn  13906  trilpolemclim  13915  trilpolemcl  13916  trilpolemisumle  13917  trilpolemeq1  13919  trilpolemlt1  13920  trilpo  13922  apdifflemf  13925  apdiff  13927  iswomni0  13930  redcwlpolemeq1  13933  redcwlpo  13934  nconstwlpolem0  13941  nconstwlpolemgt0  13942  nconstwlpo  13944  neapmkv  13946