Theorem oveq2d 6068

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 6060	. 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 6052

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 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055

This theorem is referenced by:  csbov1g  6093  caovassg  6215  caovdig  6231  caovdirg  6234  caov32d  6237  caov4d  6241  caov42d  6243  suppofss1dcl  6466  suppofss2dcl  6467  nnaass  6720  nndi  6721  nnmass  6722  nnmsucr  6723  ecovass  6880  ecoviass  6881  ecovdi  6882  ecovidi  6883  addasspig  7650  mulasspig  7652  distrpig  7653  dfplpq2  7674  mulpipq2  7691  addassnqg  7702  prarloclemarch  7738  prarloclemarch2  7739  ltrnqg  7740  enq0sym  7752  addnq0mo  7767  mulnq0mo  7768  addnnnq0  7769  nq0a0  7777  distrnq0  7779  addassnq0  7782  prarloclemlo  7814  prarloclem3  7817  prarloclem5  7820  prarloclemcalc  7822  addnqprl  7849  addnqpru  7850  prmuloclemcalc  7885  mulnqprl  7888  mulnqpru  7889  distrlem4prl  7904  distrlem4pru  7905  1idprl  7910  1idpru  7911  ltexprlemloc  7927  addcanprleml  7934  addcanprlemu  7935  recexprlem1ssu  7954  ltmprr  7962  caucvgprlemcanl  7964  cauappcvgprlemladdru  7976  cauappcvgprlemladdrl  7977  cauappcvgprlem1  7979  cauappcvgprlemlim  7981  caucvgprlemnkj  7986  caucvgprlemnbj  7987  caucvgprlemdisj  7994  caucvgprlemloc  7995  caucvgprlemcl  7996  caucvgprlemladdrl  7998  caucvgprlem1  7999  caucvgpr  8002  caucvgprprlemell  8005  caucvgprprlemcbv  8007  caucvgprprlemval  8008  caucvgprprlemnkeqj  8010  caucvgprprlemopl  8017  caucvgprprlemlol  8018  caucvgprprlemloc  8023  caucvgprprlemclphr  8025  caucvgprprlemexb  8027  caucvgprprlemaddq  8028  caucvgprprlem1  8029  addcmpblnr  8059  mulcmpblnrlemg  8060  addsrmo  8063  mulsrmo  8064  addsrpr  8065  mulsrpr  8066  ltsrprg  8067  recexgt0sr  8093  mulgt0sr  8098  caucvgsrlemgt1  8115  caucvgsrlemoffval  8116  caucvgsr  8122  suplocsrlemb  8126  suplocsrlempr  8127  suplocsrlem  8128  suplocsr  8129  mulcnsr  8155  pitoregt0  8169  recidpirqlemcalc  8177  axmulcom  8191  axmulass  8193  axdistr  8194  ax0id  8198  axcnre  8201  recriota  8210  axcaucvglemcau  8218  axcaucvglemres  8219  mulrid  8276  adddirp1d  8305  mul32  8408  mul31  8409  add32  8437  add4  8439  add42  8440  cnegex  8456  addcan2  8459  addsubass  8488  subsub2  8506  nppcan2  8509  sub32  8512  nnncan  8513  sub4  8523  muladd  8662  subdi  8663  mul2neg  8676  submul2  8677  mulsub  8679  muls1d  8696  mulsubfacd  8697  add20  8753  recexre  8857  rereim  8865  apreap  8866  ltmul1  8871  cru  8881  apreim  8882  mulreim  8883  apadd1  8887  apneg  8890  mulap0  8933  divrecap  8967  divassap  8969  divmulasscomap  8975  divsubdirap  8987  divdivdivap  8992  divmul24ap  8995  divmuleqap  8996  divcanap6  8998  divdivap1  9002  divdivap2  9003  divsubdivap  9007  conjmulap  9008  div2negap  9014  apmul1  9067  cju  9240  nnmulcl  9263  add1p1  9493  sub1m1  9494  cnm2m1cnm3  9495  xp1d2m1eqxm1d2  9496  div4p1lem1div2  9497  un0addcl  9534  un0mulcl  9535  zaddcllemneg  9621  qapne  9977  cnref1o  9989  rexsub  10192  xnegid  10198  xaddcom  10200  xnegdi  10207  xaddass  10208  xaddass2  10209  xpncan  10210  xnpcan  10211  xleadd1a  10212  xsubge0  10220  xposdif  10221  xlesubadd  10222  xadd4d  10224  lincmb01cmp  10342  iccf1o  10344  ige3m2fz  10389  fztp  10419  fzsuc2  10420  fseq1m1p1  10436  fzm1  10441  ige2m1fz1  10450  nn0split  10477  nnsplit  10478  fzo0addelr  10541  elfzoext  10544  fzval3  10556  zpnn0elfzo1  10560  fzosplitsnm1  10561  fzosplitpr  10586  fzosplitprm1  10587  fzoshftral  10591  rebtwn2zlemstep  10619  flhalf  10669  fldiv4lem1div2uz2  10673  modqval  10693  modqvalr  10694  modqdiffl  10704  modqfrac  10706  flqmod  10707  intqfrac  10708  zmod10  10709  modqmulnn  10711  modqvalp1  10712  modqid  10718  modqcyc  10728  modqcyc2  10729  modqmul1  10746  q2submod  10754  modqdi  10761  modqsubdir  10762  modqeqmodmin  10763  modsumfzodifsn  10765  addmodlteq  10767  frecuzrdgsuctlem  10792  uzsinds  10813  seqeq3  10821  iseqvalcbv  10828  seq3val  10829  seqvalcd  10830  seqf  10833  seq3p1  10834  seqovcd  10836  seqp1cd  10839  seq3m1  10842  seq3fveq2  10844  seqfveq2g  10846  seq3shft2  10850  seqshft2g  10851  monoord2  10855  ser3mono  10856  seq3split  10857  seqsplitg  10858  seq3caopr3  10860  seqcaopr3g  10861  seq3caopr2  10862  seqcaopr2g  10863  seq3caopr  10864  seqcaoprg  10865  seqf1oglem2a  10887  seqf1oglem2  10889  seq3id2  10895  seq3homo  10896  seq3z  10897  seqhomog  10899  exp3vallem  10909  exp3val  10910  expp1  10915  expnegap0  10916  expineg2  10917  expn1ap0  10918  expm1t  10936  1exp  10937  expnegzap  10942  mulexpzap  10948  expadd  10950  expaddzaplem  10951  expaddzap  10952  expmul  10953  expmulzap  10954  m1expeven  10955  expsubap  10956  expp1zap  10957  expm1ap  10958  expdivap  10959  iexpcyc  11013  subsq2  11016  binom2  11020  binom21  11021  binom2sub  11022  binom2sub1  11023  mulbinom2  11025  binom3  11026  zesq  11028  bernneq  11030  sqoddm1div8  11063  mulsubdivbinom2ap  11081  nn0opthlem1d  11090  nn0opthd  11092  facp1  11100  facnn2  11104  faclbnd  11111  faclbnd6  11114  bcval  11119  bccmpl  11124  bcn0  11125  bcnn  11127  bcnp1n  11129  bcm1k  11130  bcp1n  11131  bcp1nk  11132  bcval5  11133  bcp1m1  11135  bcpasc  11136  bcm1n  11139  bcn2m1  11140  bcn2p1  11141  omgadd  11174  hashunlem  11176  hashunsng  11180  hashdifsn  11192  hashxp  11199  hashmap  11200  sseqn  11211  zfz1isolemsplit  11218  zfz1isolem1  11220  zfz1iso  11221  seq3coll  11222  wrdf  11238  ccatfvalfi  11288  elfzelfzccat  11296  ccatlid  11302  ccatrid  11303  ccatass  11304  ccatalpha  11309  ccatws1leng  11330  ccats1val2  11336  ccatw2s1p1g  11341  swrdval  11348  swrd00g  11349  swrdf  11355  swrdfv2  11363  swrdwrdsymbg  11364  swrdspsleq  11367  swrds1  11368  swrdlsw  11369  ccatswrd  11370  swrdccat2  11371  pfxmpt  11380  pfxfv  11384  pfxeq  11396  pfxsuff1eqwrdeq  11399  ccatpfx  11401  pfxccat1  11402  swrdswrd  11405  pfxswrd  11406  swrdpfx  11407  pfxpfx  11408  pfxlswccat  11413  ccats1pfxeq  11414  ccats1pfxeqrex  11415  ccatopth2  11417  cats1un  11421  wrdind  11422  wrd2ind  11423  swrdccatfn  11424  swrdccatin1  11425  pfxccatin12lem4  11426  swrdccatin2  11429  pfxccatin12lem2c  11430  pfxccatin12lem2  11431  pfxccatin12  11433  swrdccat  11435  swrdccat3blem  11439  swrdccat3b  11440  swrdccatin2d  11444  pfxccatin12d  11445  reuccatpfxs1lem  11446  reuccatpfxs1  11447  shftcan1  11527  shftcan2  11528  cjval  11538  cjth  11539  crre  11550  replim  11552  remim  11553  reim0b  11555  rereb  11556  mulreap  11557  cjreb  11559  recj  11560  reneg  11561  readd  11562  resub  11563  remullem  11564  imcj  11568  imneg  11569  imadd  11570  imsub  11571  cjcj  11576  cjadd  11577  ipcnval  11579  cjmulrcl  11580  cjneg  11583  addcj  11584  cjsub  11585  cnrecnv  11603  caucvgrelemcau  11673  cvg1nlemcau  11677  cvg1nlemres  11678  recvguniqlem  11687  resqrexlemover  11703  resqrexlemlo  11706  resqrexlemcalc1  11707  resqrexlemcalc3  11709  resqrexlemnm  11711  resqrexlemcvg  11712  absneg  11743  abscj  11745  sqabsadd  11748  sqabssub  11749  absmul  11762  absid  11764  absre  11770  absresq  11771  absexpzap  11773  recvalap  11790  abstri  11797  abs2dif2  11800  recan  11802  cau3lem  11807  amgm2  11811  bdtrilem  11932  xrmaxadd  11954  xrbdtri  11969  climaddc1  12022  climsubc1  12025  climcvg1nlem  12042  serf0  12045  fzf1o  12069  summodclem3  12074  summodclem2a  12075  summodc  12077  fsumsplitsn  12104  fsumm1  12110  fsumsplitsnun  12113  fsump1  12114  isummulc2  12120  fsumrev  12137  fisum0diag2  12141  fsummulc2  12142  fsumsub  12146  fsumabs  12159  telfsumo  12160  fsumparts  12164  fsumrelem  12165  fsumiun  12171  binomlem  12177  binom  12178  binom1p  12179  binom11  12180  binom1dif  12181  bcxmas  12183  isumsplit  12185  isum1p  12186  divcnv  12191  arisum2  12193  trireciplem  12194  trirecip  12195  geolim  12205  georeclim  12207  geo2sum  12208  geo2lim  12210  geoisum1c  12214  0.999...  12215  cvgratnnlemnexp  12218  cvgratnnlemmn  12219  cvgratz  12226  mertenslem2  12230  mertensabs  12231  clim2prod  12233  prodfrecap  12240  prodfdivap  12241  prodmodclem3  12269  prodmodclem2a  12270  fprodm1  12292  fprodp1  12294  fprodunsn  12298  fprodfac  12309  fprodeq0  12311  fprodconst  12314  fprodrec  12323  fproddivap  12324  fprodsplitsn  12327  ege2le3  12365  efaddlem  12368  efsub  12375  efexp  12376  eftlub  12384  efsep  12385  effsumlt  12386  ef4p  12388  tanval3ap  12408  resinval  12409  recosval  12410  efi4p  12411  efival  12426  efmival  12427  efeul  12428  sinadd  12430  cosadd  12431  tanaddap  12433  sinsub  12434  cossub  12435  sincossq  12442  sin2t  12443  cos2t  12444  cos2tsin  12445  ef01bndlem  12450  sin01bnd  12451  cos01bnd  12452  cos12dec  12462  absef  12464  absefib  12465  efieq1re  12466  demoivreALT  12468  eirraplem  12471  dvdsexp  12555  oexpneg  12571  opeo  12591  omeo  12592  m1exp1  12595  flodddiv4  12630  flodddiv4t2lthalf  12633  bitsval  12637  bitsp1  12645  bitsinv1lem  12655  bitsinv1  12656  divgcdnnr  12680  gcdaddm  12688  gcdadd  12689  gcdid  12690  modgcd  12695  gcdmultipled  12697  dvdsgcdidd  12698  bezoutlemnewy  12700  bezoutlema  12703  bezoutlemb  12704  bezoutlemex  12705  bezoutlembz  12708  absmulgcd  12721  gcdmultiple  12724  gcdmultiplez  12725  rpmulgcd  12730  rplpwr  12731  eucalginv  12761  eucalg  12764  lcmneg  12779  lcmgcdlem  12782  lcmgcd  12783  lcmid  12785  lcm1  12786  mulgcddvds  12799  qredeq  12801  divgcdcoprmex  12807  prmind2  12825  rpexp1i  12859  pw2dvdslemn  12870  pw2dvdseulemle  12872  pw2dvdseu  12873  oddpwdclemxy  12874  oddpwdclemdvds  12875  oddpwdclemndvds  12876  oddpwdclemdc  12878  2sqpwodd  12881  nn0gcdsq  12905  phiprmpw  12927  eulerthlemrprm  12934  eulerthlema  12935  eulerthlemh  12936  eulerthlemth  12937  fermltl  12939  prmdiv  12940  hashgcdlem  12943  odzdvds  12951  vfermltl  12957  modprm0  12960  nnnn0modprm0  12961  modprmn0modprm0  12962  coprimeprodsq  12963  pythagtriplem1  12971  pythagtriplem4  12974  pythagtriplem12  12981  pythagtriplem14  12983  pythagtriplem16  12985  pythagtriplem18  12987  pythagtrip  12989  pcpremul  12999  pceu  13001  pczpre  13003  pcdiv  13008  pcqmul  13009  pcqdiv  13013  pcexp  13015  pcxqcl  13018  pczdvds  13020  pczndvds  13022  pczndvds2  13024  pcid  13030  pcneg  13031  pcdvdstr  13033  pcgcd1  13034  pcgcd  13035  pc2dvds  13036  pcaddlem  13045  pcadd  13046  pcadd2  13047  pcmpt  13049  pcmpt2  13050  fldivp1  13054  pcfac  13056  pcbc  13057  expnprm  13059  prmpwdvds  13061  pockthlem  13062  pockthi  13064  4sqlem7  13090  4sqlem9  13092  4sqlem10  13093  4sqlem2  13095  4sqlem3  13096  4sqlem4  13098  mul4sqlem  13099  4sqlem11  13107  4sqlem16  13112  4sqlem17  13113  4sqlem19  13115  ballotfilemfc0  13157  ballotfilemfcc  13158  setscomd  13274  ressvalsets  13298  strressid  13305  ressval3d  13306  ressinbasd  13308  ressressg  13309  ressabsg  13310  grpinvalem  13619  grpinva  13620  grprida  13621  isnsgrp  13640  sgrpass  13642  sgrp1  13645  sgrppropd  13647  prdssgrpd  13649  mnd32g  13661  mnd4g  13663  mndpropd  13674  prdsidlem  13681  prdsmndd  13682  imasmnd2  13686  mhmex  13696  mhmlin  13701  gsumwmhm  13732  grprcan  13771  grpsubval  13780  grpinvid2  13787  grpasscan2  13798  grpsubinv  13807  grpinvadd  13812  grpsubid1  13819  grpsubadd0sub  13821  grpsubadd  13822  grpsubsub  13823  grpaddsubass  13824  grppncan  13825  grpnnncan2  13831  grpsubpropd2  13839  imasgrp2  13848  mhmlem  13852  mhmid  13853  mhmmnd  13854  ghmgrp  13856  mulgnn0gsum  13866  mulgnnp1  13868  mulgaddcomlem  13883  mulgaddcom  13884  mulginvinv  13886  mulgnn0dir  13890  mulgdirlem  13891  mulgp1  13893  mulgneg2  13894  mulgnn0ass  13896  mulgass  13897  mulgmodid  13899  mulgsubdir  13900  nmzsubg  13948  0nsg  13952  eqger  13962  qussub  13975  ghmlin  13986  ghmsub  13989  conjghm  14014  ablsub4  14051  abladdsub4  14052  ablsubsub4  14057  ablsub32  14060  ablnnncan  14061  gsumfzmptfidmadd2  14078  gsumfzconst  14079  gsumfzmhm2  14082  gsumfzsnfd  14083  gsumsplit0  14084  mgpress  14096  rngass  14104  rngdi  14105  rngdir  14106  rngrz  14111  rngmneg2  14113  rngsubdi  14116  rngsubdir  14117  rngpropd  14120  imasrng  14121  srgass  14136  srgpcomp  14155  srgpcompp  14156  srgpcomppsc  14157  srg1expzeq1  14160  ringpropd  14203  ringrz  14209  ringnegr  14217  ringmneg2  14219  ringsubdi  14221  ringsubdir  14222  ring1  14224  imasring  14229  opprrng  14242  opprring  14244  mulgass3  14251  dvdsrd  14261  unitgrp  14283  invrfvald  14289  dvr1  14305  dvrass  14306  dvrcan1  14307  dvrcan3  14308  rdivmuldivd  14311  subrginv  14405  subrgdv  14406  resrhm2b  14417  rrgsupp  14434  islmod  14488  lmodlema  14489  islmodd  14490  lmodvs0  14519  lmodvneg1  14527  lmodvsubval2  14539  lmodsubvs  14540  lmodsubdi  14541  lmodsubdir  14542  lmodprop2d  14545  rmodislmodlem  14547  rmodislmod  14548  lsssn0  14567  sraval  14634  cnfldsub  14772  gsumfzfsumlem0  14783  gsumfzfsumlemm  14784  mulgrhm  14806  mulgrhm2  14807  znval  14833  znval2  14835  znunit  14856  psrval  14863  mplvalcoe  14894  mplval2g  14899  restabs  15089  cnprcl2k  15120  cnrest2r  15151  ispsmet  15237  psmettri2  15242  psmetsym  15243  ismet  15258  isxmet  15259  xmettri2  15275  xmetsym  15282  xmettri3  15288  mettri3  15289  xblss2ps  15318  xblss2  15319  comet  15413  xmetxp  15421  xmetxpbl  15422  txmetcnp  15432  fsumcncntop  15481  cncfi  15492  divcncfap  15528  limccl  15573  ellimc3apf  15574  limccnpcntop  15589  limccnp2lem  15590  reldvg  15593  dvfvalap  15595  eldvap  15596  dvcj  15623  dvfre  15624  dvexp  15625  dvexp2  15626  dvrecap  15627  dvmptaddx  15633  dvmptmulx  15634  dvmptnegcn  15636  dvmptsubcn  15637  dvmptcjx  15638  dvmptfsum  15639  dveflem  15640  dvef  15641  plyconst  15659  plyaddlem1  15661  plymullem1  15662  plyadd  15665  plymul  15666  plycoeid3  15671  plycolemc  15672  plyco  15673  plycjlemc  15674  plycj  15675  plyrecj  15677  dvply1  15679  dvply2g  15680  sin0pilem1  15695  sin0pilem2  15696  efper  15721  sinperlem  15722  efimpi  15733  ptolemy  15738  tangtx  15752  abssinper  15760  cosq34lt1  15764  rpcxpef  15808  rpcxpp1  15820  rpcxpneg  15821  rpcxpsub  15822  rpmulcxp  15823  rpdivcxp  15825  cxpmul  15826  rpcxpmul2  15827  rpcxproot  15828  cxpcom  15852  rpabscxpbnd  15854  rplogbval  15859  rplogbreexp  15867  rplogbzexp  15868  rprelogbmulexp  15870  rprelogbdiv  15871  relogbexpap  15872  rplogbcxp  15877  rpcxplogb  15878  logbgcd1irr  15881  logbgcd1irraplemap  15883  binom4  15893  pellexlem2  15895  pellexlem3  15896  wilthlem1  15897  sgmval  15900  sgmppw  15909  1sgmprm  15911  mersenne  15914  perfectlem1  15916  perfectlem2  15917  perfect  15918  lgslem1  15922  lgsval  15926  lgsfvalg  15927  lgsval2lem  15932  lgsval4  15942  lgsneg  15946  lgsneg1  15947  lgsmod  15948  lgsdir2  15955  lgsdirprm  15956  lgsdilem2  15958  lgsdi  15959  lgsne0  15960  lgssq2  15963  lgsdirnn0  15969  lgsdinn0  15970  gausslemma2dlem1a  15980  gausslemma2dlem1f1o  15982  gausslemma2dlem2  15984  gausslemma2dlem3  15985  gausslemma2dlem4  15986  gausslemma2dlem5  15988  gausslemma2dlem6  15989  gausslemma2d  15991  lgseisenlem1  15992  lgseisenlem2  15993  lgseisenlem3  15994  lgseisenlem4  15995  lgsquadlem1  15999  lgsquadlem2  16000  lgsquadlem3  16001  lgsquad2lem1  16003  lgsquad2lem2  16004  lgsquad2  16005  lgsquad3  16006  m1lgs  16007  2lgslem3c  16017  2lgslem3d  16018  2lgslem3d1  16022  2sqlem2  16037  2sqlem3  16039  2sqlem4  16040  2sqlem8  16045  2sqlem9  16046  2sqlem10  16047  vtxdumgrfival  16342  p1evtxdeqfi  16356  p1evtxdp1fi  16357  iswlk  16367  upgr2wlkdc  16421  wlkres  16423  trlreslem  16433  isclwwlk  16438  clwwlkccatlem  16444  clwwlknp  16461  clwwlkn1  16462  clwwlkn2  16465  clwwlkext2edg  16466  clwwlknonex2lem1  16481  clwwlknonex2lem2  16482  clwwlknonex2  16483  iseupth  16491  eupth2lem3lem6fi  16515  eupth2lem3lem4fi  16517  depindlem1  16550  qdencn  16856  trilpolemclim  16869  trilpolemcl  16870  trilpolemisumle  16871  trilpolemeq1  16873  trilpolemlt1  16874  trilpo  16876  apdifflemf  16879  apdiff  16881  iswomni0  16885  redcwlpolemeq1  16888  redcwlpo  16889  nconstwlpolem0  16898  nconstwlpolemgt0  16899  nconstwlpo  16901  neapmkv  16903  gfsumval  16911  gsumgfsum1  16912  gsumgfsum  16915  gfsumsn  16916  gfsump1  16917  gfsumz  16918  gfsumcl  16919