Theorem oveq2d 6023

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 6015	. 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 6007

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  csbov1g  6048  caovassg  6170  caovdig  6186  caovdirg  6189  caov32d  6192  caov4d  6196  caov42d  6198  nnaass  6639  nndi  6640  nnmass  6641  nnmsucr  6642  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  addasspig  7525  mulasspig  7527  distrpig  7528  dfplpq2  7549  mulpipq2  7566  addassnqg  7577  prarloclemarch  7613  prarloclemarch2  7614  ltrnqg  7615  enq0sym  7627  addnq0mo  7642  mulnq0mo  7643  addnnnq0  7644  nq0a0  7652  distrnq0  7654  addassnq0  7657  prarloclemlo  7689  prarloclem3  7692  prarloclem5  7695  prarloclemcalc  7697  addnqprl  7724  addnqpru  7725  prmuloclemcalc  7760  mulnqprl  7763  mulnqpru  7764  distrlem4prl  7779  distrlem4pru  7780  1idprl  7785  1idpru  7786  ltexprlemloc  7802  addcanprleml  7809  addcanprlemu  7810  recexprlem1ssu  7829  ltmprr  7837  caucvgprlemcanl  7839  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  cauappcvgprlem1  7854  cauappcvgprlemlim  7856  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprlemdisj  7869  caucvgprlemloc  7870  caucvgprlemcl  7871  caucvgprlemladdrl  7873  caucvgprlem1  7874  caucvgpr  7877  caucvgprprlemell  7880  caucvgprprlemcbv  7882  caucvgprprlemval  7883  caucvgprprlemnkeqj  7885  caucvgprprlemopl  7892  caucvgprprlemlol  7893  caucvgprprlemloc  7898  caucvgprprlemclphr  7900  caucvgprprlemexb  7902  caucvgprprlemaddq  7903  caucvgprprlem1  7904  addcmpblnr  7934  mulcmpblnrlemg  7935  addsrmo  7938  mulsrmo  7939  addsrpr  7940  mulsrpr  7941  ltsrprg  7942  recexgt0sr  7968  mulgt0sr  7973  caucvgsrlemgt1  7990  caucvgsrlemoffval  7991  caucvgsr  7997  suplocsrlemb  8001  suplocsrlempr  8002  suplocsrlem  8003  suplocsr  8004  mulcnsr  8030  pitoregt0  8044  recidpirqlemcalc  8052  axmulcom  8066  axmulass  8068  axdistr  8069  ax0id  8073  axcnre  8076  recriota  8085  axcaucvglemcau  8093  axcaucvglemres  8094  mulrid  8151  adddirp1d  8181  mul32  8284  mul31  8285  add32  8313  add4  8315  add42  8316  cnegex  8332  addcan2  8335  addsubass  8364  subsub2  8382  nppcan2  8385  sub32  8388  nnncan  8389  sub4  8399  muladd  8538  subdi  8539  mul2neg  8552  submul2  8553  mulsub  8555  muls1d  8572  mulsubfacd  8573  add20  8629  recexre  8733  rereim  8741  apreap  8742  ltmul1  8747  cru  8757  apreim  8758  mulreim  8759  apadd1  8763  apneg  8766  mulap0  8809  divrecap  8843  divassap  8845  divmulasscomap  8851  divsubdirap  8863  divdivdivap  8868  divmul24ap  8871  divmuleqap  8872  divcanap6  8874  divdivap1  8878  divdivap2  8879  divsubdivap  8883  conjmulap  8884  div2negap  8890  apmul1  8943  cju  9116  nnmulcl  9139  add1p1  9369  sub1m1  9370  cnm2m1cnm3  9371  xp1d2m1eqxm1d2  9372  div4p1lem1div2  9373  un0addcl  9410  un0mulcl  9411  zaddcllemneg  9493  qapne  9842  cnref1o  9854  rexsub  10057  xnegid  10063  xaddcom  10065  xnegdi  10072  xaddass  10073  xaddass2  10074  xpncan  10075  xnpcan  10076  xleadd1a  10077  xsubge0  10085  xposdif  10086  xlesubadd  10087  xadd4d  10089  lincmb01cmp  10207  iccf1o  10208  ige3m2fz  10253  fztp  10282  fzsuc2  10283  fseq1m1p1  10299  fzm1  10304  ige2m1fz1  10313  nn0split  10340  nnsplit  10341  fzo0addelr  10403  elfzoext  10406  fzval3  10418  zpnn0elfzo1  10422  fzosplitsnm1  10423  fzosplitprm1  10448  fzoshftral  10452  rebtwn2zlemstep  10480  flhalf  10530  fldiv4lem1div2uz2  10534  modqval  10554  modqvalr  10555  modqdiffl  10565  modqfrac  10567  flqmod  10568  intqfrac  10569  zmod10  10570  modqmulnn  10572  modqvalp1  10573  modqid  10579  modqcyc  10589  modqcyc2  10590  modqmul1  10607  q2submod  10615  modqdi  10622  modqsubdir  10623  modqeqmodmin  10624  modsumfzodifsn  10626  addmodlteq  10628  frecuzrdgsuctlem  10653  uzsinds  10674  seqeq3  10682  iseqvalcbv  10689  seq3val  10690  seqvalcd  10691  seqf  10694  seq3p1  10695  seqovcd  10697  seqp1cd  10700  seq3m1  10703  seq3fveq2  10705  seqfveq2g  10707  seq3shft2  10711  seqshft2g  10712  monoord2  10716  ser3mono  10717  seq3split  10718  seqsplitg  10719  seq3caopr3  10721  seqcaopr3g  10722  seq3caopr2  10723  seqcaopr2g  10724  seq3caopr  10725  seqcaoprg  10726  seqf1oglem2a  10748  seqf1oglem2  10750  seq3id2  10756  seq3homo  10757  seq3z  10758  seqhomog  10760  exp3vallem  10770  exp3val  10771  expp1  10776  expnegap0  10777  expineg2  10778  expn1ap0  10779  expm1t  10797  1exp  10798  expnegzap  10803  mulexpzap  10809  expadd  10811  expaddzaplem  10812  expaddzap  10813  expmul  10814  expmulzap  10815  m1expeven  10816  expsubap  10817  expp1zap  10818  expm1ap  10819  expdivap  10820  iexpcyc  10874  subsq2  10877  binom2  10881  binom21  10882  binom2sub  10883  binom2sub1  10884  mulbinom2  10886  binom3  10887  zesq  10888  bernneq  10890  sqoddm1div8  10923  mulsubdivbinom2ap  10941  nn0opthlem1d  10950  nn0opthd  10952  facp1  10960  facnn2  10964  faclbnd  10971  faclbnd6  10974  bcval  10979  bccmpl  10984  bcn0  10985  bcnn  10987  bcnp1n  10989  bcm1k  10990  bcp1n  10991  bcp1nk  10992  bcval5  10993  bcp1m1  10995  bcpasc  10996  bcn2m1  10999  bcn2p1  11000  omgadd  11032  hashunlem  11034  hashunsng  11037  hashdifsn  11049  hashxp  11056  zfz1isolemsplit  11068  zfz1isolem1  11070  zfz1iso  11071  seq3coll  11072  wrdf  11085  ccatfvalfi  11135  elfzelfzccat  11143  ccatlid  11149  ccatrid  11150  ccatass  11151  ccatws1leng  11175  ccats1val2  11179  swrdval  11188  swrd00g  11189  swrdf  11195  swrdfv2  11203  swrdwrdsymbg  11204  swrdspsleq  11207  swrds1  11208  swrdlsw  11209  ccatswrd  11210  swrdccat2  11211  pfxmpt  11220  pfxfv  11224  pfxeq  11236  pfxsuff1eqwrdeq  11239  ccatpfx  11241  pfxccat1  11242  swrdswrd  11245  pfxswrd  11246  swrdpfx  11247  pfxpfx  11248  pfxlswccat  11253  ccats1pfxeq  11254  ccats1pfxeqrex  11255  ccatopth2  11257  cats1un  11261  wrdind  11262  wrd2ind  11263  swrdccatfn  11264  swrdccatin1  11265  pfxccatin12lem4  11266  swrdccatin2  11269  pfxccatin12lem2c  11270  pfxccatin12lem2  11271  pfxccatin12  11273  swrdccat  11275  swrdccat3blem  11279  swrdccat3b  11280  swrdccatin2d  11284  pfxccatin12d  11285  reuccatpfxs1lem  11286  reuccatpfxs1  11287  shftcan1  11353  shftcan2  11354  cjval  11364  cjth  11365  crre  11376  replim  11378  remim  11379  reim0b  11381  rereb  11382  mulreap  11383  cjreb  11385  recj  11386  reneg  11387  readd  11388  resub  11389  remullem  11390  imcj  11394  imneg  11395  imadd  11396  imsub  11397  cjcj  11402  cjadd  11403  ipcnval  11405  cjmulrcl  11406  cjneg  11409  addcj  11410  cjsub  11411  cnrecnv  11429  caucvgrelemcau  11499  cvg1nlemcau  11503  cvg1nlemres  11504  recvguniqlem  11513  resqrexlemover  11529  resqrexlemlo  11532  resqrexlemcalc1  11533  resqrexlemcalc3  11535  resqrexlemnm  11537  resqrexlemcvg  11538  absneg  11569  abscj  11571  sqabsadd  11574  sqabssub  11575  absmul  11588  absid  11590  absre  11596  absresq  11597  absexpzap  11599  recvalap  11616  abstri  11623  abs2dif2  11626  recan  11628  cau3lem  11633  amgm2  11637  bdtrilem  11758  xrmaxadd  11780  xrbdtri  11795  climaddc1  11848  climsubc1  11851  climcvg1nlem  11868  serf0  11871  summodclem3  11899  summodclem2a  11900  summodc  11902  fsumsplitsn  11929  fsumm1  11935  fsumsplitsnun  11938  fsump1  11939  isummulc2  11945  fsumrev  11962  fisum0diag2  11966  fsummulc2  11967  fsumsub  11971  fsumabs  11984  telfsumo  11985  fsumparts  11989  fsumrelem  11990  fsumiun  11996  binomlem  12002  binom  12003  binom1p  12004  binom11  12005  binom1dif  12006  bcxmas  12008  isumsplit  12010  isum1p  12011  divcnv  12016  arisum2  12018  trireciplem  12019  trirecip  12020  geolim  12030  georeclim  12032  geo2sum  12033  geo2lim  12035  geoisum1c  12039  0.999...  12040  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  cvgratz  12051  mertenslem2  12055  mertensabs  12056  clim2prod  12058  prodfrecap  12065  prodfdivap  12066  prodmodclem3  12094  prodmodclem2a  12095  fprodm1  12117  fprodp1  12119  fprodunsn  12123  fprodfac  12134  fprodeq0  12136  fprodconst  12139  fprodrec  12148  fproddivap  12149  fprodsplitsn  12152  ege2le3  12190  efaddlem  12193  efsub  12200  efexp  12201  eftlub  12209  efsep  12210  effsumlt  12211  ef4p  12213  tanval3ap  12233  resinval  12234  recosval  12235  efi4p  12236  efival  12251  efmival  12252  efeul  12253  sinadd  12255  cosadd  12256  tanaddap  12258  sinsub  12259  cossub  12260  sincossq  12267  sin2t  12268  cos2t  12269  cos2tsin  12270  ef01bndlem  12275  sin01bnd  12276  cos01bnd  12277  cos12dec  12287  absef  12289  absefib  12290  efieq1re  12291  demoivreALT  12293  eirraplem  12296  dvdsexp  12380  oexpneg  12396  opeo  12416  omeo  12417  m1exp1  12420  flodddiv4  12455  flodddiv4t2lthalf  12458  bitsval  12462  bitsp1  12470  bitsinv1lem  12480  bitsinv1  12481  divgcdnnr  12505  gcdaddm  12513  gcdadd  12514  gcdid  12515  modgcd  12520  gcdmultipled  12522  dvdsgcdidd  12523  bezoutlemnewy  12525  bezoutlema  12528  bezoutlemb  12529  bezoutlemex  12530  bezoutlembz  12533  absmulgcd  12546  gcdmultiple  12549  gcdmultiplez  12550  rpmulgcd  12555  rplpwr  12556  eucalginv  12586  eucalg  12589  lcmneg  12604  lcmgcdlem  12607  lcmgcd  12608  lcmid  12610  lcm1  12611  mulgcddvds  12624  qredeq  12626  divgcdcoprmex  12632  prmind2  12650  rpexp1i  12684  pw2dvdslemn  12695  pw2dvdseulemle  12697  pw2dvdseu  12698  oddpwdclemxy  12699  oddpwdclemdvds  12700  oddpwdclemndvds  12701  oddpwdclemdc  12703  2sqpwodd  12706  nn0gcdsq  12730  phiprmpw  12752  eulerthlemrprm  12759  eulerthlema  12760  eulerthlemh  12761  eulerthlemth  12762  fermltl  12764  prmdiv  12765  hashgcdlem  12768  odzdvds  12776  vfermltl  12782  modprm0  12785  nnnn0modprm0  12786  modprmn0modprm0  12787  coprimeprodsq  12788  pythagtriplem1  12796  pythagtriplem4  12799  pythagtriplem12  12806  pythagtriplem14  12808  pythagtriplem16  12810  pythagtriplem18  12812  pythagtrip  12814  pcpremul  12824  pceu  12826  pczpre  12828  pcdiv  12833  pcqmul  12834  pcqdiv  12838  pcexp  12840  pcxqcl  12843  pczdvds  12845  pczndvds  12847  pczndvds2  12849  pcid  12855  pcneg  12856  pcdvdstr  12858  pcgcd1  12859  pcgcd  12860  pc2dvds  12861  pcaddlem  12870  pcadd  12871  pcadd2  12872  pcmpt  12874  pcmpt2  12875  fldivp1  12879  pcfac  12881  pcbc  12882  expnprm  12884  prmpwdvds  12886  pockthlem  12887  pockthi  12889  4sqlem7  12915  4sqlem9  12917  4sqlem10  12918  4sqlem2  12920  4sqlem3  12921  4sqlem4  12923  mul4sqlem  12924  4sqlem11  12932  4sqlem16  12937  4sqlem17  12938  4sqlem19  12940  setscomd  13081  ressvalsets  13105  strressid  13112  ressval3d  13113  ressinbasd  13115  ressressg  13116  ressabsg  13117  grpinvalem  13426  grpinva  13427  grprida  13428  isnsgrp  13447  sgrpass  13449  sgrp1  13452  sgrppropd  13454  prdssgrpd  13456  mnd32g  13468  mnd4g  13470  mndpropd  13481  prdsidlem  13488  prdsmndd  13489  imasmnd2  13493  mhmex  13503  mhmlin  13508  gsumwmhm  13539  grprcan  13578  grpsubval  13587  grpinvid2  13594  grpasscan2  13605  grpsubinv  13614  grpinvadd  13619  grpsubid1  13626  grpsubadd0sub  13628  grpsubadd  13629  grpsubsub  13630  grpaddsubass  13631  grppncan  13632  grpnnncan2  13638  grpsubpropd2  13646  imasgrp2  13655  mhmlem  13659  mhmid  13660  mhmmnd  13661  ghmgrp  13663  mulgnn0gsum  13673  mulgnnp1  13675  mulgaddcomlem  13690  mulgaddcom  13691  mulginvinv  13693  mulgnn0dir  13697  mulgdirlem  13698  mulgp1  13700  mulgneg2  13701  mulgnn0ass  13703  mulgass  13704  mulgmodid  13706  mulgsubdir  13707  nmzsubg  13755  0nsg  13759  eqger  13769  qussub  13782  ghmlin  13793  ghmsub  13796  conjghm  13821  ablsub4  13858  abladdsub4  13859  ablsubsub4  13864  ablsub32  13867  ablnnncan  13868  gsumfzmptfidmadd2  13885  gsumfzconst  13886  gsumfzmhm2  13889  gsumfzsnfd  13890  mgpress  13902  rngass  13910  rngdi  13911  rngdir  13912  rngrz  13917  rngmneg2  13919  rngsubdi  13922  rngsubdir  13923  rngpropd  13926  imasrng  13927  srgass  13942  srgpcomp  13961  srgpcompp  13962  srgpcomppsc  13963  srg1expzeq1  13966  ringpropd  14009  ringrz  14015  ringnegr  14023  ringmneg2  14025  ringsubdi  14027  ringsubdir  14028  ring1  14030  imasring  14035  opprrng  14048  opprring  14050  mulgass3  14056  dvdsrd  14066  unitgrp  14088  invrfvald  14094  dvr1  14110  dvrass  14111  dvrcan1  14112  dvrcan3  14113  rdivmuldivd  14116  subrginv  14209  subrgdv  14210  resrhm2b  14221  islmod  14263  lmodlema  14264  islmodd  14265  lmodvs0  14294  lmodvneg1  14302  lmodvsubval2  14314  lmodsubvs  14315  lmodsubdi  14316  lmodsubdir  14317  lmodprop2d  14320  rmodislmodlem  14322  rmodislmod  14323  lsssn0  14342  sraval  14409  cnfldsub  14547  gsumfzfsumlem0  14558  gsumfzfsumlemm  14559  mulgrhm  14581  mulgrhm2  14582  znval  14608  znval2  14610  znunit  14631  psrval  14638  mplvalcoe  14662  mplval2g  14667  restabs  14857  cnprcl2k  14888  cnrest2r  14919  ispsmet  15005  psmettri2  15010  psmetsym  15011  ismet  15026  isxmet  15027  xmettri2  15043  xmetsym  15050  xmettri3  15056  mettri3  15057  xblss2ps  15086  xblss2  15087  comet  15181  xmetxp  15189  xmetxpbl  15190  txmetcnp  15200  fsumcncntop  15249  cncfi  15260  divcncfap  15296  limccl  15341  ellimc3apf  15342  limccnpcntop  15357  limccnp2lem  15358  reldvg  15361  dvfvalap  15363  eldvap  15364  dvcj  15391  dvfre  15392  dvexp  15393  dvexp2  15394  dvrecap  15395  dvmptaddx  15401  dvmptmulx  15402  dvmptnegcn  15404  dvmptsubcn  15405  dvmptcjx  15406  dvmptfsum  15407  dveflem  15408  dvef  15409  plyconst  15427  plyaddlem1  15429  plymullem1  15430  plyadd  15433  plymul  15434  plycoeid3  15439  plycolemc  15440  plyco  15441  plycjlemc  15442  plycj  15443  plyrecj  15445  dvply1  15447  dvply2g  15448  sin0pilem1  15463  sin0pilem2  15464  efper  15489  sinperlem  15490  efimpi  15501  ptolemy  15506  tangtx  15520  abssinper  15528  cosq34lt1  15532  rpcxpef  15576  rpcxpp1  15588  rpcxpneg  15589  rpcxpsub  15590  rpmulcxp  15591  rpdivcxp  15593  cxpmul  15594  rpcxpmul2  15595  rpcxproot  15596  cxpcom  15620  rpabscxpbnd  15622  rplogbval  15627  rplogbreexp  15635  rplogbzexp  15636  rprelogbmulexp  15638  rprelogbdiv  15639  relogbexpap  15640  rplogbcxp  15645  rpcxplogb  15646  logbgcd1irr  15649  logbgcd1irraplemap  15651  binom4  15661  wilthlem1  15662  sgmval  15665  sgmppw  15674  1sgmprm  15676  mersenne  15679  perfectlem1  15681  perfectlem2  15682  perfect  15683  lgslem1  15687  lgsval  15691  lgsfvalg  15692  lgsval2lem  15697  lgsval4  15707  lgsneg  15711  lgsneg1  15712  lgsmod  15713  lgsdir2  15720  lgsdirprm  15721  lgsdilem2  15723  lgsdi  15724  lgsne0  15725  lgssq2  15728  lgsdirnn0  15734  lgsdinn0  15735  gausslemma2dlem1a  15745  gausslemma2dlem1f1o  15747  gausslemma2dlem2  15749  gausslemma2dlem3  15750  gausslemma2dlem4  15751  gausslemma2dlem5  15753  gausslemma2dlem6  15754  gausslemma2d  15756  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem3  15759  lgseisenlem4  15760  lgsquadlem1  15764  lgsquadlem2  15765  lgsquadlem3  15766  lgsquad2lem1  15768  lgsquad2lem2  15769  lgsquad2  15770  lgsquad3  15771  m1lgs  15772  2lgslem3c  15782  2lgslem3d  15783  2lgslem3d1  15787  2sqlem2  15802  2sqlem3  15804  2sqlem4  15805  2sqlem8  15810  2sqlem9  15811  2sqlem10  15812  iswlk  16044  upgr2wlkdc  16096  wlkres  16098  trlreslem  16107  qdencn  16425  trilpolemclim  16434  trilpolemcl  16435  trilpolemisumle  16436  trilpolemeq1  16438  trilpolemlt1  16439  trilpo  16441  apdifflemf  16444  apdiff  16446  iswomni0  16449  redcwlpolemeq1  16452  redcwlpo  16453  nconstwlpolem0  16461  nconstwlpolemgt0  16462  nconstwlpo  16464  neapmkv  16466