Theorem oveq2d 6074

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 6066	. 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 1398  (class class class)co 6058

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  csbov1g  6099  caovassg  6221  caovdig  6237  caovdirg  6240  caov32d  6243  caov4d  6247  caov42d  6249  suppofss1dcl  6477  suppofss2dcl  6478  nnaass  6731  nndi  6732  nnmass  6733  nnmsucr  6734  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  addasspig  7661  mulasspig  7663  distrpig  7664  dfplpq2  7685  mulpipq2  7702  addassnqg  7713  prarloclemarch  7749  prarloclemarch2  7750  ltrnqg  7751  enq0sym  7763  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  nq0a0  7788  distrnq0  7790  addassnq0  7793  prarloclemlo  7825  prarloclem3  7828  prarloclem5  7831  prarloclemcalc  7833  addnqprl  7860  addnqpru  7861  prmuloclemcalc  7896  mulnqprl  7899  mulnqpru  7900  distrlem4prl  7915  distrlem4pru  7916  1idprl  7921  1idpru  7922  ltexprlemloc  7938  addcanprleml  7945  addcanprlemu  7946  recexprlem1ssu  7965  ltmprr  7973  caucvgprlemcanl  7975  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  cauappcvgprlem1  7990  cauappcvgprlemlim  7992  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemdisj  8005  caucvgprlemloc  8006  caucvgprlemcl  8007  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgpr  8013  caucvgprprlemell  8016  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemnkeqj  8021  caucvgprprlemopl  8028  caucvgprprlemlol  8029  caucvgprprlemloc  8034  caucvgprprlemclphr  8036  caucvgprprlemexb  8038  caucvgprprlemaddq  8039  caucvgprprlem1  8040  addcmpblnr  8070  mulcmpblnrlemg  8071  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  ltsrprg  8078  recexgt0sr  8104  mulgt0sr  8109  caucvgsrlemgt1  8126  caucvgsrlemoffval  8127  caucvgsr  8133  suplocsrlemb  8137  suplocsrlempr  8138  suplocsrlem  8139  suplocsr  8140  mulcnsr  8166  pitoregt0  8180  recidpirqlemcalc  8188  axmulcom  8202  axmulass  8204  axdistr  8205  ax0id  8209  axcnre  8212  recriota  8221  axcaucvglemcau  8229  axcaucvglemres  8230  mulrid  8287  adddirp1d  8316  mul32  8420  mul31  8421  add32  8449  add4  8451  add42  8452  cnegex  8468  addcan2  8471  addsubass  8500  subsub2  8518  nppcan2  8521  sub32  8524  nnncan  8525  sub4  8535  muladd  8675  subdi  8676  mul2neg  8689  submul2  8690  mulsub  8692  muls1d  8709  mulsubfacd  8710  add20  8766  recexre  8870  rereim  8878  apreap  8879  ltmul1  8884  cru  8894  apreim  8895  mulreim  8896  apadd1  8900  apneg  8903  mulap0  8946  divrecap  8982  divassap  8984  divmulasscomap  8990  divsubdirap  9002  divdivdivap  9007  divmul24ap  9010  divmuleqap  9011  divcanap6  9013  divdivap1  9017  divdivap2  9018  divsubdivap  9022  conjmulap  9023  div2negap  9029  apmul1  9082  cju  9255  nnmulcl  9278  add1p1  9508  sub1m1  9509  cnm2m1cnm3  9510  xp1d2m1eqxm1d2  9511  div4p1lem1div2  9512  un0addcl  9549  un0mulcl  9550  zaddcllemneg  9636  qapne  9992  cnref1o  10004  rexsub  10208  xnegid  10214  xaddcom  10216  xnegdi  10223  xaddass  10224  xaddass2  10225  xpncan  10226  xnpcan  10227  xleadd1a  10228  xsubge0  10236  xposdif  10237  xlesubadd  10238  xadd4d  10240  lincmb01cmp  10358  iccf1o  10360  ige3m2fz  10406  fztp  10437  fzsuc2  10438  fseq1m1p1  10454  fzm1  10459  ige2m1fz1  10468  nn0split  10495  nnsplit  10496  fzo0addelr  10559  elfzoext  10562  fzval3  10574  zpnn0elfzo1  10578  fzosplitsnm1  10579  fzosplitpr  10604  fzosplitprm1  10605  fzoshftral  10609  rebtwn2zlemstep  10639  flhalf  10689  fldiv4lem1div2uz2  10693  modqval  10713  modqvalr  10714  modqdiffl  10724  modqfrac  10726  flqmod  10727  intqfrac  10728  zmod10  10729  modqmulnn  10731  modqvalp1  10732  modqid  10738  modqcyc  10748  modqcyc2  10749  modqmul1  10766  q2submod  10774  modqdi  10781  modqsubdir  10782  modqeqmodmin  10783  modsumfzodifsn  10785  addmodlteq  10787  frecuzrdgsuctlem  10812  uzsinds  10833  seqeq3  10841  iseqvalcbv  10848  seq3val  10849  seqvalcd  10850  seqf  10853  seq3p1  10854  seqovcd  10856  seqp1cd  10859  seq3m1  10862  seq3fveq2  10864  seqfveq2g  10866  seq3shft2  10870  seqshft2g  10871  monoord2  10875  ser3mono  10876  seq3split  10877  seqsplitg  10878  seq3caopr3  10880  seqcaopr3g  10881  seq3caopr2  10882  seqcaopr2g  10883  seq3caopr  10884  seqcaoprg  10885  seqf1oglem2a  10907  seqf1oglem2  10909  seq3id2  10915  seq3homo  10916  seq3z  10917  seqhomog  10919  exp3vallem  10929  exp3val  10930  expp1  10935  expnegap0  10936  expineg2  10937  expn1ap0  10938  expm1t  10956  1exp  10957  expnegzap  10962  mulexpzap  10968  expadd  10970  expaddzaplem  10971  expaddzap  10972  expmul  10973  expmulzap  10974  m1expeven  10975  expsubap  10976  expp1zap  10977  expm1ap  10978  expdivap  10979  iexpcyc  11033  subsq2  11036  binom2  11040  binom21  11041  binom2sub  11042  binom2sub1  11043  mulbinom2  11045  binom3  11046  zesq  11048  bernneq  11050  sqoddm1div8  11083  mulsubdivbinom2ap  11101  nn0opthlem1d  11110  nn0opthd  11112  facp1  11120  facnn2  11124  faclbnd  11131  faclbnd6  11134  bcval  11139  bccmpl  11144  bcn0  11145  bcnn  11147  bcnp1n  11149  bcm1k  11150  bcp1n  11151  bcp1nk  11152  bcval5  11153  bcp1m1  11155  bcpasc  11156  bcm1n  11159  bcn2m1  11160  bcn2p1  11161  omgadd  11194  hashunlem  11196  hashunsng  11200  hashdifsn  11212  hashxp  11219  hashmap  11220  sseqn  11231  zfz1isolemsplit  11238  zfz1isolem1  11240  zfz1iso  11241  seq3coll  11242  wrdf  11258  ccatfvalfi  11308  elfzelfzccat  11316  ccatlid  11322  ccatrid  11323  ccatass  11324  ccatalpha  11329  ccatws1leng  11350  ccats1val2  11356  ccatw2s1p1g  11361  swrdval  11368  swrd00g  11369  swrdf  11375  swrdfv2  11383  swrdwrdsymbg  11384  swrdspsleq  11387  swrds1  11388  swrdlsw  11389  ccatswrd  11390  swrdccat2  11391  pfxmpt  11400  pfxfv  11404  pfxeq  11416  pfxsuff1eqwrdeq  11419  ccatpfx  11421  pfxccat1  11422  swrdswrd  11425  pfxswrd  11426  swrdpfx  11427  pfxpfx  11428  pfxlswccat  11433  ccats1pfxeq  11434  ccats1pfxeqrex  11435  ccatopth2  11437  cats1un  11441  wrdind  11442  wrd2ind  11443  swrdccatfn  11444  swrdccatin1  11445  pfxccatin12lem4  11446  swrdccatin2  11449  pfxccatin12lem2c  11450  pfxccatin12lem2  11451  pfxccatin12  11453  swrdccat  11455  swrdccat3blem  11459  swrdccat3b  11460  swrdccatin2d  11464  pfxccatin12d  11465  reuccatpfxs1lem  11466  reuccatpfxs1  11467  shftcan1  11547  shftcan2  11548  cjval  11558  cjth  11559  crre  11570  replim  11572  remim  11573  reim0b  11575  rereb  11576  mulreap  11577  cjreb  11579  recj  11580  reneg  11581  readd  11582  resub  11583  remullem  11584  imcj  11588  imneg  11589  imadd  11590  imsub  11591  cjcj  11596  cjadd  11597  ipcnval  11599  cjmulrcl  11600  cjneg  11603  addcj  11604  cjsub  11605  cnrecnv  11623  caucvgrelemcau  11693  cvg1nlemcau  11697  cvg1nlemres  11698  recvguniqlem  11707  resqrexlemover  11723  resqrexlemlo  11726  resqrexlemcalc1  11727  resqrexlemcalc3  11729  resqrexlemnm  11731  resqrexlemcvg  11732  absneg  11763  abscj  11765  sqabsadd  11768  sqabssub  11769  absmul  11782  absid  11784  absre  11790  absresq  11791  absexpzap  11793  recvalap  11810  abstri  11817  abs2dif2  11820  recan  11822  cau3lem  11827  amgm2  11831  bdtrilem  11952  xrmaxadd  11974  xrbdtri  11989  climaddc1  12042  climsubc1  12045  climcvg1nlem  12062  serf0  12065  fzf1o  12089  summodclem3  12094  summodclem2a  12095  summodc  12097  fsumsplitsn  12124  fsumm1  12130  fsumsplitsnun  12133  fsump1  12134  isummulc2  12140  fsumrev  12157  fisum0diag2  12161  fsummulc2  12162  fsumsub  12166  fsumabs  12179  telfsumo  12180  fsumparts  12184  fsumrelem  12185  fsumiun  12191  binomlem  12197  binom  12198  binom1p  12199  binom11  12200  binom1dif  12201  bcxmas  12203  isumsplit  12205  isum1p  12206  divcnv  12211  arisum2  12213  trireciplem  12214  trirecip  12215  geolim  12225  georeclim  12227  geo2sum  12228  geo2lim  12230  geoisum1c  12234  0.999...  12235  cvgratnnlemnexp  12238  cvgratnnlemmn  12239  cvgratz  12246  mertenslem2  12250  mertensabs  12251  clim2prod  12253  prodfrecap  12260  prodfdivap  12261  prodmodclem3  12289  prodmodclem2a  12290  fprodm1  12312  fprodp1  12314  fprodunsn  12318  fprodfac  12329  fprodeq0  12331  fprodconst  12334  fprodrec  12343  fproddivap  12344  fprodsplitsn  12347  ege2le3  12385  efaddlem  12388  efsub  12395  efexp  12396  eftlub  12404  efsep  12405  effsumlt  12406  ef4p  12408  tanval3ap  12428  resinval  12429  recosval  12430  efi4p  12431  efival  12446  efmival  12447  efeul  12448  sinadd  12450  cosadd  12451  tanaddap  12453  sinsub  12454  cossub  12455  sincossq  12462  sin2t  12463  cos2t  12464  cos2tsin  12465  ef01bndlem  12470  sin01bnd  12471  cos01bnd  12472  cos12dec  12482  absef  12484  absefib  12485  efieq1re  12486  demoivreALT  12488  eirraplem  12491  dvdsexp  12575  oexpneg  12591  opeo  12611  omeo  12612  m1exp1  12615  flodddiv4  12650  flodddiv4t2lthalf  12653  bitsval  12657  bitsp1  12665  bitsinv1lem  12675  bitsinv1  12676  divgcdnnr  12700  gcdaddm  12708  gcdadd  12709  gcdid  12710  modgcd  12715  gcdmultipled  12717  dvdsgcdidd  12718  bezoutlemnewy  12720  bezoutlema  12723  bezoutlemb  12724  bezoutlemex  12725  bezoutlembz  12728  absmulgcd  12741  gcdmultiple  12744  gcdmultiplez  12745  rpmulgcd  12750  rplpwr  12751  eucalginv  12781  eucalg  12784  lcmneg  12799  lcmgcdlem  12802  lcmgcd  12803  lcmid  12805  lcm1  12806  mulgcddvds  12819  qredeq  12821  divgcdcoprmex  12827  prmind2  12845  rpexp1i  12879  pw2dvdslemn  12890  pw2dvdseulemle  12892  pw2dvdseu  12893  oddpwdclemxy  12894  oddpwdclemdvds  12895  oddpwdclemndvds  12896  oddpwdclemdc  12898  2sqpwodd  12901  nn0gcdsq  12925  phiprmpw  12947  eulerthlemrprm  12954  eulerthlema  12955  eulerthlemh  12956  eulerthlemth  12957  fermltl  12959  prmdiv  12960  hashgcdlem  12963  odzdvds  12971  vfermltl  12977  modprm0  12980  nnnn0modprm0  12981  modprmn0modprm0  12982  coprimeprodsq  12983  pythagtriplem1  12991  pythagtriplem4  12994  pythagtriplem12  13001  pythagtriplem14  13003  pythagtriplem16  13005  pythagtriplem18  13007  pythagtrip  13009  pcpremul  13019  pceu  13021  pczpre  13023  pcdiv  13028  pcqmul  13029  pcqdiv  13033  pcexp  13035  pcxqcl  13038  pczdvds  13040  pczndvds  13042  pczndvds2  13044  pcid  13050  pcneg  13051  pcdvdstr  13053  pcgcd1  13054  pcgcd  13055  pc2dvds  13056  pcaddlem  13065  pcadd  13066  pcadd2  13067  pcmpt  13069  pcmpt2  13070  fldivp1  13074  pcfac  13076  pcbc  13077  expnprm  13079  prmpwdvds  13081  pockthlem  13082  pockthi  13084  4sqlem7  13110  4sqlem9  13112  4sqlem10  13113  4sqlem2  13115  4sqlem3  13116  4sqlem4  13118  mul4sqlem  13119  4sqlem11  13127  4sqlem16  13132  4sqlem17  13133  4sqlem19  13135  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilemsv  13200  ballotfilemsima  13206  ballotfilemfrci  13218  setscomd  13340  ressvalsets  13364  strressid  13371  ressval3d  13372  ressinbasd  13374  ressressg  13375  ressabsg  13376  grpinvalem  13651  grpinva  13652  grprida  13653  isnsgrp  13672  sgrpass  13674  sgrp1  13677  sgrppropd  13679  mnd32g  13691  mnd4g  13693  mndpropd  13704  imasmnd2  13710  mhmex  13720  mhmlin  13725  gsumwmhm  13756  grprcan  13795  grpsubval  13804  grpinvid2  13811  grpasscan2  13822  grpsubinv  13831  grpinvadd  13836  grpsubid1  13843  grpsubadd0sub  13845  grpsubadd  13846  grpsubsub  13847  grpaddsubass  13848  grppncan  13849  grpnnncan2  13855  grpsubpropd2  13863  imasgrp2  13866  mhmlem  13870  mhmid  13871  mhmmnd  13872  ghmgrp  13874  mulgnn0gsum  13884  mulgnnp1  13886  mulgaddcomlem  13901  mulgaddcom  13902  mulginvinv  13904  mulgnn0dir  13908  mulgdirlem  13909  mulgp1  13911  mulgneg2  13912  mulgnn0ass  13914  mulgass  13915  mulgmodid  13917  mulgsubdir  13918  nmzsubg  13966  0nsg  13970  eqger  13980  qussub  13993  ghmlin  14004  ghmsub  14007  conjghm  14032  ablsub4  14069  abladdsub4  14070  ablsubsub4  14075  ablsub32  14078  ablnnncan  14079  gsumfzmptfidmadd2  14096  gsumfzconst  14097  gsumfzmhm2  14100  gsumfzsnfd  14101  gsumsplit0  14102  gfsumval  14105  gsumgfsum1  14106  gsumgfsum  14109  gfsumsn  14110  gfsump1  14111  gfsumz  14112  gfsumcl  14113  prdssgrpd  14136  prdsidlem  14138  prdsmndd  14139  mgpress  14173  rngass  14181  rngdi  14182  rngdir  14183  rngrz  14188  rngmneg2  14190  rngsubdi  14193  rngsubdir  14194  rngpropd  14197  imasrng  14198  srgass  14217  srgpcomp  14236  srgpcompp  14237  srgpcomppsc  14238  srg1expzeq1  14241  ringpropd  14284  ringrz  14290  ringnegr  14298  ringmneg2  14300  ringsubdi  14302  ringsubdir  14303  ring1  14305  imasring  14310  opprrng  14323  opprring  14325  mulgass3  14332  dvdsrd  14342  unitgrp  14364  invrfvald  14370  dvr1  14386  dvrass  14387  dvrcan1  14388  dvrcan3  14389  rdivmuldivd  14392  subrginv  14486  subrgdv  14487  resrhm2b  14498  rrgsupp  14515  islmod  14568  lmodlema  14569  islmodd  14570  lmodvs0  14599  lmodvneg1  14607  lmodvsubval2  14619  lmodsubvs  14620  lmodsubdi  14621  lmodsubdir  14622  lmodprop2d  14625  rmodislmodlem  14627  rmodislmod  14628  lsssn0  14647  sraval  14714  cnfldsub  14852  gsumfzfsumlem0  14863  gsumfzfsumlemm  14864  mulgrhm  14886  mulgrhm2  14887  znval  14913  znval2  14915  znunit  14936  psrval  14943  mplvalcoe  14974  mplval2g  14979  restabs  15169  cnprcl2k  15200  cnrest2r  15231  ispsmet  15317  psmettri2  15322  psmetsym  15323  ismet  15338  isxmet  15339  xmettri2  15355  xmetsym  15362  xmettri3  15368  mettri3  15369  xblss2ps  15398  xblss2  15399  comet  15493  xmetxp  15501  xmetxpbl  15502  txmetcnp  15512  fsumcncntop  15561  cncfi  15572  divcncfap  15608  limccl  15653  ellimc3apf  15654  limccnpcntop  15669  limccnp2lem  15670  reldvg  15673  dvfvalap  15675  eldvap  15676  dvcj  15703  dvfre  15704  dvexp  15705  dvexp2  15706  dvrecap  15707  dvmptaddx  15713  dvmptmulx  15714  dvmptnegcn  15716  dvmptsubcn  15717  dvmptcjx  15718  dvmptfsum  15719  dveflem  15720  dvef  15721  plyconst  15739  plyaddlem1  15741  plymullem1  15742  plyadd  15745  plymul  15746  plycoeid3  15751  plycolemc  15752  plyco  15753  plycjlemc  15754  plycj  15755  plyrecj  15757  dvply1  15759  dvply2g  15760  sin0pilem1  15775  sin0pilem2  15776  efper  15801  sinperlem  15802  efimpi  15813  ptolemy  15818  tangtx  15832  abssinper  15840  cosq34lt1  15844  rpcxpef  15888  rpcxpp1  15900  rpcxpneg  15901  rpcxpsub  15902  rpmulcxp  15903  rpdivcxp  15905  cxpmul  15906  rpcxpmul2  15907  rpcxproot  15908  cxpcom  15932  rpabscxpbnd  15934  rplogbval  15939  rplogbreexp  15947  rplogbzexp  15948  rprelogbmulexp  15950  rprelogbdiv  15951  relogbexpap  15952  rplogbcxp  15957  rpcxplogb  15958  logbgcd1irr  15961  logbgcd1irraplemap  15963  binom4  15973  pellexlem2  15975  pellexlem3  15976  wilthlem1  15977  sgmval  15980  sgmppw  15989  1sgmprm  15991  mersenne  15994  perfectlem1  15996  perfectlem2  15997  perfect  15998  lgslem1  16002  lgsval  16006  lgsfvalg  16007  lgsval2lem  16012  lgsval4  16022  lgsneg  16026  lgsneg1  16027  lgsmod  16028  lgsdir2  16035  lgsdirprm  16036  lgsdilem2  16038  lgsdi  16039  lgsne0  16040  lgssq2  16043  lgsdirnn0  16049  lgsdinn0  16050  gausslemma2dlem1a  16060  gausslemma2dlem1f1o  16062  gausslemma2dlem2  16064  gausslemma2dlem3  16065  gausslemma2dlem4  16066  gausslemma2dlem5  16068  gausslemma2dlem6  16069  gausslemma2d  16071  lgseisenlem1  16072  lgseisenlem2  16073  lgseisenlem3  16074  lgseisenlem4  16075  lgsquadlem1  16079  lgsquadlem2  16080  lgsquadlem3  16081  lgsquad2lem1  16083  lgsquad2lem2  16084  lgsquad2  16085  lgsquad3  16086  m1lgs  16087  2lgslem3c  16097  2lgslem3d  16098  2lgslem3d1  16102  2sqlem2  16117  2sqlem3  16119  2sqlem4  16120  2sqlem8  16125  2sqlem9  16126  2sqlem10  16127  vtxdumgrfival  16422  p1evtxdeqfi  16436  p1evtxdp1fi  16437  iswlk  16447  upgr2wlkdc  16501  wlkres  16503  trlreslem  16513  isclwwlk  16518  clwwlkccatlem  16524  clwwlknp  16541  clwwlkn1  16542  clwwlkn2  16545  clwwlkext2edg  16546  clwwlknonex2lem1  16561  clwwlknonex2lem2  16562  clwwlknonex2  16563  iseupth  16571  eupth2lem3lem6fi  16595  eupth2lem3lem4fi  16597  depindlem1  16630  qdencn  16946  trilpolemclim  16959  trilpolemcl  16960  trilpolemisumle  16961  trilpolemeq1  16963  trilpolemlt1  16964  trilpo  16966  apdifflemf  16969  apdiff  16971  iswomni0  16975  redcwlpolemeq1  16978  redcwlpo  16979  nconstwlpolem0  16988  nconstwlpolemgt0  16989  nconstwlpo  16991  neapmkv  16993