Theorem oveq2d 6039

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 6031	. 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 6023

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 2212

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1810  df-clab 2217  df-cleq 2223  df-clel 2226  df-nfc 2362  df-rex 2515  df-v 2803  df-un 3203  df-sn 3676  df-pr 3677  df-op 3679  df-uni 3895  df-br 4090  df-iota 5288  df-fv 5336  df-ov 6026

This theorem is referenced by:  csbov1g  6064  caovassg  6186  caovdig  6202  caovdirg  6205  caov32d  6208  caov4d  6212  caov42d  6214  nnaass  6658  nndi  6659  nnmass  6660  nnmsucr  6661  ecovass  6818  ecoviass  6819  ecovdi  6820  ecovidi  6821  addasspig  7555  mulasspig  7557  distrpig  7558  dfplpq2  7579  mulpipq2  7596  addassnqg  7607  prarloclemarch  7643  prarloclemarch2  7644  ltrnqg  7645  enq0sym  7657  addnq0mo  7672  mulnq0mo  7673  addnnnq0  7674  nq0a0  7682  distrnq0  7684  addassnq0  7687  prarloclemlo  7719  prarloclem3  7722  prarloclem5  7725  prarloclemcalc  7727  addnqprl  7754  addnqpru  7755  prmuloclemcalc  7790  mulnqprl  7793  mulnqpru  7794  distrlem4prl  7809  distrlem4pru  7810  1idprl  7815  1idpru  7816  ltexprlemloc  7832  addcanprleml  7839  addcanprlemu  7840  recexprlem1ssu  7859  ltmprr  7867  caucvgprlemcanl  7869  cauappcvgprlemladdru  7881  cauappcvgprlemladdrl  7882  cauappcvgprlem1  7884  cauappcvgprlemlim  7886  caucvgprlemnkj  7891  caucvgprlemnbj  7892  caucvgprlemdisj  7899  caucvgprlemloc  7900  caucvgprlemcl  7901  caucvgprlemladdrl  7903  caucvgprlem1  7904  caucvgpr  7907  caucvgprprlemell  7910  caucvgprprlemcbv  7912  caucvgprprlemval  7913  caucvgprprlemnkeqj  7915  caucvgprprlemopl  7922  caucvgprprlemlol  7923  caucvgprprlemloc  7928  caucvgprprlemclphr  7930  caucvgprprlemexb  7932  caucvgprprlemaddq  7933  caucvgprprlem1  7934  addcmpblnr  7964  mulcmpblnrlemg  7965  addsrmo  7968  mulsrmo  7969  addsrpr  7970  mulsrpr  7971  ltsrprg  7972  recexgt0sr  7998  mulgt0sr  8003  caucvgsrlemgt1  8020  caucvgsrlemoffval  8021  caucvgsr  8027  suplocsrlemb  8031  suplocsrlempr  8032  suplocsrlem  8033  suplocsr  8034  mulcnsr  8060  pitoregt0  8074  recidpirqlemcalc  8082  axmulcom  8096  axmulass  8098  axdistr  8099  ax0id  8103  axcnre  8106  recriota  8115  axcaucvglemcau  8123  axcaucvglemres  8124  mulrid  8181  adddirp1d  8211  mul32  8314  mul31  8315  add32  8343  add4  8345  add42  8346  cnegex  8362  addcan2  8365  addsubass  8394  subsub2  8412  nppcan2  8415  sub32  8418  nnncan  8419  sub4  8429  muladd  8568  subdi  8569  mul2neg  8582  submul2  8583  mulsub  8585  muls1d  8602  mulsubfacd  8603  add20  8659  recexre  8763  rereim  8771  apreap  8772  ltmul1  8777  cru  8787  apreim  8788  mulreim  8789  apadd1  8793  apneg  8796  mulap0  8839  divrecap  8873  divassap  8875  divmulasscomap  8881  divsubdirap  8893  divdivdivap  8898  divmul24ap  8901  divmuleqap  8902  divcanap6  8904  divdivap1  8908  divdivap2  8909  divsubdivap  8913  conjmulap  8914  div2negap  8920  apmul1  8973  cju  9146  nnmulcl  9169  add1p1  9399  sub1m1  9400  cnm2m1cnm3  9401  xp1d2m1eqxm1d2  9402  div4p1lem1div2  9403  un0addcl  9440  un0mulcl  9441  zaddcllemneg  9523  qapne  9878  cnref1o  9890  rexsub  10093  xnegid  10099  xaddcom  10101  xnegdi  10108  xaddass  10109  xaddass2  10110  xpncan  10111  xnpcan  10112  xleadd1a  10113  xsubge0  10121  xposdif  10122  xlesubadd  10123  xadd4d  10125  lincmb01cmp  10243  iccf1o  10244  ige3m2fz  10289  fztp  10318  fzsuc2  10319  fseq1m1p1  10335  fzm1  10340  ige2m1fz1  10349  nn0split  10376  nnsplit  10377  fzo0addelr  10440  elfzoext  10443  fzval3  10455  zpnn0elfzo1  10459  fzosplitsnm1  10460  fzosplitpr  10485  fzosplitprm1  10486  fzoshftral  10490  rebtwn2zlemstep  10518  flhalf  10568  fldiv4lem1div2uz2  10572  modqval  10592  modqvalr  10593  modqdiffl  10603  modqfrac  10605  flqmod  10606  intqfrac  10607  zmod10  10608  modqmulnn  10610  modqvalp1  10611  modqid  10617  modqcyc  10627  modqcyc2  10628  modqmul1  10645  q2submod  10653  modqdi  10660  modqsubdir  10661  modqeqmodmin  10662  modsumfzodifsn  10664  addmodlteq  10666  frecuzrdgsuctlem  10691  uzsinds  10712  seqeq3  10720  iseqvalcbv  10727  seq3val  10728  seqvalcd  10729  seqf  10732  seq3p1  10733  seqovcd  10735  seqp1cd  10738  seq3m1  10741  seq3fveq2  10743  seqfveq2g  10745  seq3shft2  10749  seqshft2g  10750  monoord2  10754  ser3mono  10755  seq3split  10756  seqsplitg  10757  seq3caopr3  10759  seqcaopr3g  10760  seq3caopr2  10761  seqcaopr2g  10762  seq3caopr  10763  seqcaoprg  10764  seqf1oglem2a  10786  seqf1oglem2  10788  seq3id2  10794  seq3homo  10795  seq3z  10796  seqhomog  10798  exp3vallem  10808  exp3val  10809  expp1  10814  expnegap0  10815  expineg2  10816  expn1ap0  10817  expm1t  10835  1exp  10836  expnegzap  10841  mulexpzap  10847  expadd  10849  expaddzaplem  10850  expaddzap  10851  expmul  10852  expmulzap  10853  m1expeven  10854  expsubap  10855  expp1zap  10856  expm1ap  10857  expdivap  10858  iexpcyc  10912  subsq2  10915  binom2  10919  binom21  10920  binom2sub  10921  binom2sub1  10922  mulbinom2  10924  binom3  10925  zesq  10926  bernneq  10928  sqoddm1div8  10961  mulsubdivbinom2ap  10979  nn0opthlem1d  10988  nn0opthd  10990  facp1  10998  facnn2  11002  faclbnd  11009  faclbnd6  11012  bcval  11017  bccmpl  11022  bcn0  11023  bcnn  11025  bcnp1n  11027  bcm1k  11028  bcp1n  11029  bcp1nk  11030  bcval5  11031  bcp1m1  11033  bcpasc  11034  bcn2m1  11037  bcn2p1  11038  omgadd  11071  hashunlem  11073  hashunsng  11077  hashdifsn  11089  hashxp  11096  zfz1isolemsplit  11108  zfz1isolem1  11110  zfz1iso  11111  seq3coll  11112  wrdf  11128  ccatfvalfi  11178  elfzelfzccat  11186  ccatlid  11192  ccatrid  11193  ccatass  11194  ccatalpha  11199  ccatws1leng  11220  ccats1val2  11226  ccatw2s1p1g  11231  swrdval  11238  swrd00g  11239  swrdf  11245  swrdfv2  11253  swrdwrdsymbg  11254  swrdspsleq  11257  swrds1  11258  swrdlsw  11259  ccatswrd  11260  swrdccat2  11261  pfxmpt  11270  pfxfv  11274  pfxeq  11286  pfxsuff1eqwrdeq  11289  ccatpfx  11291  pfxccat1  11292  swrdswrd  11295  pfxswrd  11296  swrdpfx  11297  pfxpfx  11298  pfxlswccat  11303  ccats1pfxeq  11304  ccats1pfxeqrex  11305  ccatopth2  11307  cats1un  11311  wrdind  11312  wrd2ind  11313  swrdccatfn  11314  swrdccatin1  11315  pfxccatin12lem4  11316  swrdccatin2  11319  pfxccatin12lem2c  11320  pfxccatin12lem2  11321  pfxccatin12  11323  swrdccat  11325  swrdccat3blem  11329  swrdccat3b  11330  swrdccatin2d  11334  pfxccatin12d  11335  reuccatpfxs1lem  11336  reuccatpfxs1  11337  shftcan1  11417  shftcan2  11418  cjval  11428  cjth  11429  crre  11440  replim  11442  remim  11443  reim0b  11445  rereb  11446  mulreap  11447  cjreb  11449  recj  11450  reneg  11451  readd  11452  resub  11453  remullem  11454  imcj  11458  imneg  11459  imadd  11460  imsub  11461  cjcj  11466  cjadd  11467  ipcnval  11469  cjmulrcl  11470  cjneg  11473  addcj  11474  cjsub  11475  cnrecnv  11493  caucvgrelemcau  11563  cvg1nlemcau  11567  cvg1nlemres  11568  recvguniqlem  11577  resqrexlemover  11593  resqrexlemlo  11596  resqrexlemcalc1  11597  resqrexlemcalc3  11599  resqrexlemnm  11601  resqrexlemcvg  11602  absneg  11633  abscj  11635  sqabsadd  11638  sqabssub  11639  absmul  11652  absid  11654  absre  11660  absresq  11661  absexpzap  11663  recvalap  11680  abstri  11687  abs2dif2  11690  recan  11692  cau3lem  11697  amgm2  11701  bdtrilem  11822  xrmaxadd  11844  xrbdtri  11859  climaddc1  11912  climsubc1  11915  climcvg1nlem  11932  serf0  11935  fzf1o  11959  summodclem3  11964  summodclem2a  11965  summodc  11967  fsumsplitsn  11994  fsumm1  12000  fsumsplitsnun  12003  fsump1  12004  isummulc2  12010  fsumrev  12027  fisum0diag2  12031  fsummulc2  12032  fsumsub  12036  fsumabs  12049  telfsumo  12050  fsumparts  12054  fsumrelem  12055  fsumiun  12061  binomlem  12067  binom  12068  binom1p  12069  binom11  12070  binom1dif  12071  bcxmas  12073  isumsplit  12075  isum1p  12076  divcnv  12081  arisum2  12083  trireciplem  12084  trirecip  12085  geolim  12095  georeclim  12097  geo2sum  12098  geo2lim  12100  geoisum1c  12104  0.999...  12105  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  cvgratz  12116  mertenslem2  12120  mertensabs  12121  clim2prod  12123  prodfrecap  12130  prodfdivap  12131  prodmodclem3  12159  prodmodclem2a  12160  fprodm1  12182  fprodp1  12184  fprodunsn  12188  fprodfac  12199  fprodeq0  12201  fprodconst  12204  fprodrec  12213  fproddivap  12214  fprodsplitsn  12217  ege2le3  12255  efaddlem  12258  efsub  12265  efexp  12266  eftlub  12274  efsep  12275  effsumlt  12276  ef4p  12278  tanval3ap  12298  resinval  12299  recosval  12300  efi4p  12301  efival  12316  efmival  12317  efeul  12318  sinadd  12320  cosadd  12321  tanaddap  12323  sinsub  12324  cossub  12325  sincossq  12332  sin2t  12333  cos2t  12334  cos2tsin  12335  ef01bndlem  12340  sin01bnd  12341  cos01bnd  12342  cos12dec  12352  absef  12354  absefib  12355  efieq1re  12356  demoivreALT  12358  eirraplem  12361  dvdsexp  12445  oexpneg  12461  opeo  12481  omeo  12482  m1exp1  12485  flodddiv4  12520  flodddiv4t2lthalf  12523  bitsval  12527  bitsp1  12535  bitsinv1lem  12545  bitsinv1  12546  divgcdnnr  12570  gcdaddm  12578  gcdadd  12579  gcdid  12580  modgcd  12585  gcdmultipled  12587  dvdsgcdidd  12588  bezoutlemnewy  12590  bezoutlema  12593  bezoutlemb  12594  bezoutlemex  12595  bezoutlembz  12598  absmulgcd  12611  gcdmultiple  12614  gcdmultiplez  12615  rpmulgcd  12620  rplpwr  12621  eucalginv  12651  eucalg  12654  lcmneg  12669  lcmgcdlem  12672  lcmgcd  12673  lcmid  12675  lcm1  12676  mulgcddvds  12689  qredeq  12691  divgcdcoprmex  12697  prmind2  12715  rpexp1i  12749  pw2dvdslemn  12760  pw2dvdseulemle  12762  pw2dvdseu  12763  oddpwdclemxy  12764  oddpwdclemdvds  12765  oddpwdclemndvds  12766  oddpwdclemdc  12768  2sqpwodd  12771  nn0gcdsq  12795  phiprmpw  12817  eulerthlemrprm  12824  eulerthlema  12825  eulerthlemh  12826  eulerthlemth  12827  fermltl  12829  prmdiv  12830  hashgcdlem  12833  odzdvds  12841  vfermltl  12847  modprm0  12850  nnnn0modprm0  12851  modprmn0modprm0  12852  coprimeprodsq  12853  pythagtriplem1  12861  pythagtriplem4  12864  pythagtriplem12  12871  pythagtriplem14  12873  pythagtriplem16  12875  pythagtriplem18  12877  pythagtrip  12879  pcpremul  12889  pceu  12891  pczpre  12893  pcdiv  12898  pcqmul  12899  pcqdiv  12903  pcexp  12905  pcxqcl  12908  pczdvds  12910  pczndvds  12912  pczndvds2  12914  pcid  12920  pcneg  12921  pcdvdstr  12923  pcgcd1  12924  pcgcd  12925  pc2dvds  12926  pcaddlem  12935  pcadd  12936  pcadd2  12937  pcmpt  12939  pcmpt2  12940  fldivp1  12944  pcfac  12946  pcbc  12947  expnprm  12949  prmpwdvds  12951  pockthlem  12952  pockthi  12954  4sqlem7  12980  4sqlem9  12982  4sqlem10  12983  4sqlem2  12985  4sqlem3  12986  4sqlem4  12988  mul4sqlem  12989  4sqlem11  12997  4sqlem16  13002  4sqlem17  13003  4sqlem19  13005  setscomd  13146  ressvalsets  13170  strressid  13177  ressval3d  13178  ressinbasd  13180  ressressg  13181  ressabsg  13182  grpinvalem  13491  grpinva  13492  grprida  13493  isnsgrp  13512  sgrpass  13514  sgrp1  13517  sgrppropd  13519  prdssgrpd  13521  mnd32g  13533  mnd4g  13535  mndpropd  13546  prdsidlem  13553  prdsmndd  13554  imasmnd2  13558  mhmex  13568  mhmlin  13573  gsumwmhm  13604  grprcan  13643  grpsubval  13652  grpinvid2  13659  grpasscan2  13670  grpsubinv  13679  grpinvadd  13684  grpsubid1  13691  grpsubadd0sub  13693  grpsubadd  13694  grpsubsub  13695  grpaddsubass  13696  grppncan  13697  grpnnncan2  13703  grpsubpropd2  13711  imasgrp2  13720  mhmlem  13724  mhmid  13725  mhmmnd  13726  ghmgrp  13728  mulgnn0gsum  13738  mulgnnp1  13740  mulgaddcomlem  13755  mulgaddcom  13756  mulginvinv  13758  mulgnn0dir  13762  mulgdirlem  13763  mulgp1  13765  mulgneg2  13766  mulgnn0ass  13768  mulgass  13769  mulgmodid  13771  mulgsubdir  13772  nmzsubg  13820  0nsg  13824  eqger  13834  qussub  13847  ghmlin  13858  ghmsub  13861  conjghm  13886  ablsub4  13923  abladdsub4  13924  ablsubsub4  13929  ablsub32  13932  ablnnncan  13933  gsumfzmptfidmadd2  13950  gsumfzconst  13951  gsumfzmhm2  13954  gsumfzsnfd  13955  gsumsplit0  13956  mgpress  13968  rngass  13976  rngdi  13977  rngdir  13978  rngrz  13983  rngmneg2  13985  rngsubdi  13988  rngsubdir  13989  rngpropd  13992  imasrng  13993  srgass  14008  srgpcomp  14027  srgpcompp  14028  srgpcomppsc  14029  srg1expzeq1  14032  ringpropd  14075  ringrz  14081  ringnegr  14089  ringmneg2  14091  ringsubdi  14093  ringsubdir  14094  ring1  14096  imasring  14101  opprrng  14114  opprring  14116  mulgass3  14122  dvdsrd  14132  unitgrp  14154  invrfvald  14160  dvr1  14176  dvrass  14177  dvrcan1  14178  dvrcan3  14179  rdivmuldivd  14182  subrginv  14275  subrgdv  14276  resrhm2b  14287  islmod  14329  lmodlema  14330  islmodd  14331  lmodvs0  14360  lmodvneg1  14368  lmodvsubval2  14380  lmodsubvs  14381  lmodsubdi  14382  lmodsubdir  14383  lmodprop2d  14386  rmodislmodlem  14388  rmodislmod  14389  lsssn0  14408  sraval  14475  cnfldsub  14613  gsumfzfsumlem0  14624  gsumfzfsumlemm  14625  mulgrhm  14647  mulgrhm2  14648  znval  14674  znval2  14676  znunit  14697  psrval  14704  mplvalcoe  14733  mplval2g  14738  restabs  14928  cnprcl2k  14959  cnrest2r  14990  ispsmet  15076  psmettri2  15081  psmetsym  15082  ismet  15097  isxmet  15098  xmettri2  15114  xmetsym  15121  xmettri3  15127  mettri3  15128  xblss2ps  15157  xblss2  15158  comet  15252  xmetxp  15260  xmetxpbl  15261  txmetcnp  15271  fsumcncntop  15320  cncfi  15331  divcncfap  15367  limccl  15412  ellimc3apf  15413  limccnpcntop  15428  limccnp2lem  15429  reldvg  15432  dvfvalap  15434  eldvap  15435  dvcj  15462  dvfre  15463  dvexp  15464  dvexp2  15465  dvrecap  15466  dvmptaddx  15472  dvmptmulx  15473  dvmptnegcn  15475  dvmptsubcn  15476  dvmptcjx  15477  dvmptfsum  15478  dveflem  15479  dvef  15480  plyconst  15498  plyaddlem1  15500  plymullem1  15501  plyadd  15504  plymul  15505  plycoeid3  15510  plycolemc  15511  plyco  15512  plycjlemc  15513  plycj  15514  plyrecj  15516  dvply1  15518  dvply2g  15519  sin0pilem1  15534  sin0pilem2  15535  efper  15560  sinperlem  15561  efimpi  15572  ptolemy  15577  tangtx  15591  abssinper  15599  cosq34lt1  15603  rpcxpef  15647  rpcxpp1  15659  rpcxpneg  15660  rpcxpsub  15661  rpmulcxp  15662  rpdivcxp  15664  cxpmul  15665  rpcxpmul2  15666  rpcxproot  15667  cxpcom  15691  rpabscxpbnd  15693  rplogbval  15698  rplogbreexp  15706  rplogbzexp  15707  rprelogbmulexp  15709  rprelogbdiv  15710  relogbexpap  15711  rplogbcxp  15716  rpcxplogb  15717  logbgcd1irr  15720  logbgcd1irraplemap  15722  binom4  15732  wilthlem1  15733  sgmval  15736  sgmppw  15745  1sgmprm  15747  mersenne  15750  perfectlem1  15752  perfectlem2  15753  perfect  15754  lgslem1  15758  lgsval  15762  lgsfvalg  15763  lgsval2lem  15768  lgsval4  15778  lgsneg  15782  lgsneg1  15783  lgsmod  15784  lgsdir2  15791  lgsdirprm  15792  lgsdilem2  15794  lgsdi  15795  lgsne0  15796  lgssq2  15799  lgsdirnn0  15805  lgsdinn0  15806  gausslemma2dlem1a  15816  gausslemma2dlem1f1o  15818  gausslemma2dlem2  15820  gausslemma2dlem3  15821  gausslemma2dlem4  15822  gausslemma2dlem5  15824  gausslemma2dlem6  15825  gausslemma2d  15827  lgseisenlem1  15828  lgseisenlem2  15829  lgseisenlem3  15830  lgseisenlem4  15831  lgsquadlem1  15835  lgsquadlem2  15836  lgsquadlem3  15837  lgsquad2lem1  15839  lgsquad2lem2  15840  lgsquad2  15841  lgsquad3  15842  m1lgs  15843  2lgslem3c  15853  2lgslem3d  15854  2lgslem3d1  15858  2sqlem2  15873  2sqlem3  15875  2sqlem4  15876  2sqlem8  15881  2sqlem9  15882  2sqlem10  15883  vtxdumgrfival  16178  p1evtxdeqfi  16192  p1evtxdp1fi  16193  iswlk  16203  upgr2wlkdc  16257  wlkres  16259  trlreslem  16269  isclwwlk  16274  clwwlkccatlem  16280  clwwlknp  16297  clwwlkn1  16298  clwwlkn2  16301  clwwlkext2edg  16302  clwwlknonex2lem1  16317  clwwlknonex2lem2  16318  clwwlknonex2  16319  iseupth  16327  eupth2lem3lem6fi  16351  eupth2lem3lem4fi  16353  depindlem1  16386  qdencn  16694  trilpolemclim  16707  trilpolemcl  16708  trilpolemisumle  16709  trilpolemeq1  16711  trilpolemlt1  16712  trilpo  16714  apdifflemf  16717  apdiff  16719  iswomni0  16723  redcwlpolemeq1  16726  redcwlpo  16727  nconstwlpolem0  16735  nconstwlpolemgt0  16736  nconstwlpo  16738  neapmkv  16740  gfsumval  16748  gsumgfsum1  16749  gsumgfsum  16752  gfsumsn  16753  gfsump1  16754  gfsumcl  16755