Theorem oveq2d 6101

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 6093	. 2 |- ( A = B -> ( C F A ) = ( C F B ) )
3	1, 2	syl 14	1 |- ( ph -> ( C F A ) = ( C F B ) )

This proof depends on syntax axioms:   -> wi 4   = wceq 1402  (class class class)co 6085

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  csbov1g  6126  caovassg  6248  caovdig  6264  caovdirg  6267  caov32d  6270  caov4d  6274  caov42d  6276  suppofss1dcl  6504  suppofss2dcl  6505  nnaass  6758  nndi  6759  nnmass  6760  nnmsucr  6761  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  addasspig  7697  mulasspig  7699  distrpig  7700  dfplpq2  7721  mulpipq2  7738  addassnqg  7749  prarloclemarch  7785  prarloclemarch2  7786  ltrnqg  7787  enq0sym  7799  addnq0mo  7814  mulnq0mo  7815  addnnnq0  7816  nq0a0  7824  distrnq0  7826  addassnq0  7829  prarloclemlo  7861  prarloclem3  7864  prarloclem5  7867  prarloclemcalc  7869  addnqprl  7896  addnqpru  7897  prmuloclemcalc  7932  mulnqprl  7935  mulnqpru  7936  distrlem4prl  7951  distrlem4pru  7952  1idprl  7957  1idpru  7958  ltexprlemloc  7974  addcanprleml  7981  addcanprlemu  7982  recexprlem1ssu  8001  ltmprr  8009  caucvgprlemcanl  8011  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  cauappcvgprlem1  8026  cauappcvgprlemlim  8028  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemdisj  8041  caucvgprlemloc  8042  caucvgprlemcl  8043  caucvgprlemladdrl  8045  caucvgprlem1  8046  caucvgpr  8049  caucvgprprlemell  8052  caucvgprprlemcbv  8054  caucvgprprlemval  8055  caucvgprprlemnkeqj  8057  caucvgprprlemopl  8064  caucvgprprlemlol  8065  caucvgprprlemloc  8070  caucvgprprlemclphr  8072  caucvgprprlemexb  8074  caucvgprprlemaddq  8075  caucvgprprlem1  8076  addcmpblnr  8106  mulcmpblnrlemg  8107  addsrmo  8110  mulsrmo  8111  addsrpr  8112  mulsrpr  8113  ltsrprg  8114  recexgt0sr  8140  mulgt0sr  8145  caucvgsrlemgt1  8162  caucvgsrlemoffval  8163  caucvgsr  8169  suplocsrlemb  8173  suplocsrlempr  8174  suplocsrlem  8175  suplocsr  8176  mulcnsr  8202  pitoregt0  8216  recidpirqlemcalc  8224  axmulcom  8238  axmulass  8240  axdistr  8241  ax0id  8245  axcnre  8248  recriota  8257  axcaucvglemcau  8265  axcaucvglemres  8266  mulrid  8323  adddirp1d  8352  mul32  8456  mul31  8457  add32  8485  add4  8487  add42  8488  cnegex  8504  addcan2  8507  addsubass  8536  subsub2  8554  nppcan2  8557  sub32  8560  nnncan  8561  sub4  8571  muladd  8711  subdi  8712  mul2neg  8725  submul2  8726  mulsub  8728  muls1d  8745  mulsubfacd  8746  add20  8802  recexre  8907  rereim  8915  apreap  8916  ltmul1  8921  cru  8931  apreim  8932  mulreim  8933  apadd1  8937  apneg  8940  mulap0  8983  divrecap  9019  divassap  9021  divmulasscomap  9027  divsubdirap  9039  divdivdivap  9044  divmul24ap  9047  divmuleqap  9048  divcanap6  9050  divdivap1  9054  divdivap2  9055  divsubdivap  9059  conjmulap  9060  div2negap  9066  apmul1  9119  cju  9292  nnmulcl  9326  add1p1  9557  sub1m1  9558  cnm2m1cnm3  9559  xp1d2m1eqxm1d2  9560  div4p1lem1div2  9561  un0addcl  9598  un0mulcl  9599  zaddcllemneg  9685  qapne  10041  cnref1o  10053  rexsub  10257  xnegid  10263  xaddcom  10265  xnegdi  10272  xaddass  10273  xaddass2  10274  xpncan  10275  xnpcan  10276  xleadd1a  10277  xsubge0  10285  xposdif  10286  xlesubadd  10287  xadd4d  10289  lincmb01cmp  10407  iccf1o  10409  ige3m2fz  10456  fztp  10487  fzsuc2  10488  fseq1m1p1  10504  fzm1  10509  ige2m1fz1  10518  nn0split  10545  nnsplit  10546  fzo0addelr  10609  elfzoext  10612  fzval3  10624  zpnn0elfzo1  10628  fzosplitsnm1  10629  fzosplitpr  10654  fzosplitprm1  10655  fzoshftral  10659  rebtwn2zlemstep  10689  flhalf  10739  fldiv4lem1div2uz2  10743  modqval  10763  modqvalr  10764  modqdiffl  10774  modqfrac  10776  flqmod  10777  intqfrac  10778  zmod10  10779  modqmulnn  10781  modqvalp1  10782  modqid  10788  modqcyc  10798  modqcyc2  10799  modqmul1  10816  q2submod  10824  modqdi  10831  modqsubdir  10832  modqeqmodmin  10833  modsumfzodifsn  10835  addmodlteq  10837  frecuzrdgsuctlem  10862  uzsinds  10883  seqeq3  10891  iseqvalcbv  10898  seq3val  10899  seqvalcd  10900  seqf  10903  seq3p1  10904  seqovcd  10906  seqp1cd  10909  seq3m1  10912  seq3fveq2  10914  seqfveq2g  10916  seq3shft2  10920  seqshft2g  10921  monoord2  10925  ser3mono  10926  seq3split  10927  seqsplitg  10928  seq3caopr3  10930  seqcaopr3g  10931  seq3caopr2  10932  seqcaopr2g  10933  seq3caopr  10934  seqcaoprg  10935  seqf1oglem2a  10957  seqf1oglem2  10959  seq3id2  10965  seq3homo  10966  seq3z  10967  seqhomog  10969  exp3vallem  10979  exp3val  10980  expp1  10985  expnegap0  10986  expineg2  10987  expn1ap0  10988  expm1t  11006  1exp  11007  expnegzap  11012  mulexpzap  11018  expadd  11020  expaddzaplem  11021  expaddzap  11022  expmul  11023  expmulzap  11024  m1expeven  11025  expsubap  11026  expp1zap  11027  expm1ap  11028  expdivap  11029  iexpcyc  11083  subsq2  11086  binom2  11090  binom21  11091  binom2sub  11092  binom2sub1  11093  mulbinom2  11095  binom3  11096  zesq  11098  bernneq  11100  sqoddm1div8  11133  mulsubdivbinom2ap  11151  nn0opthlem1d  11160  nn0opthd  11162  facp1  11170  facnn2  11174  faclbnd  11181  faclbnd6  11184  bcval  11189  bccmpl  11194  bcn0  11195  bcnn  11197  bcnp1n  11199  bcm1k  11200  bcp1n  11201  bcp1nk  11202  bcval5  11203  bcp1m1  11205  bcpasc  11206  bcm1n  11209  bcn2m1  11210  bcn2p1  11211  omgadd  11244  hashunlem  11246  hashunsng  11250  hashdifsn  11262  hashxp  11269  hashmap  11270  sseqn  11281  hashf1lem2  11288  hashf1  11289  hashfac  11290  zfz1isolemsplit  11292  zfz1isolem1  11294  zfz1iso  11295  seq3coll  11296  wrdf  11312  ccatfvalfi  11362  elfzelfzccat  11370  ccatlid  11376  ccatrid  11377  ccatass  11378  ccatalpha  11383  ccatws1leng  11404  ccats1val2  11410  ccatw2s1p1g  11415  swrdval  11422  swrd00g  11423  swrdf  11429  swrdfv2  11437  swrdwrdsymbg  11438  swrdspsleq  11441  swrds1  11442  swrdlsw  11443  ccatswrd  11444  swrdccat2  11445  pfxmpt  11454  pfxfv  11458  pfxeq  11470  pfxsuff1eqwrdeq  11473  ccatpfx  11475  pfxccat1  11476  swrdswrd  11479  pfxswrd  11480  swrdpfx  11481  pfxpfx  11482  pfxlswccat  11487  ccats1pfxeq  11488  ccats1pfxeqrex  11489  ccatopth2  11491  cats1un  11495  wrdind  11496  wrd2ind  11497  swrdccatfn  11498  swrdccatin1  11499  pfxccatin12lem4  11500  swrdccatin2  11503  pfxccatin12lem2c  11504  pfxccatin12lem2  11505  pfxccatin12  11507  swrdccat  11509  swrdccat3blem  11513  swrdccat3b  11514  swrdccatin2d  11518  pfxccatin12d  11519  reuccatpfxs1lem  11520  reuccatpfxs1  11521  shftcan1  11601  shftcan2  11602  cjval  11612  cjth  11613  crre  11624  replim  11626  remim  11627  reim0b  11629  rereb  11630  mulreap  11631  cjreb  11633  recj  11634  reneg  11635  readd  11636  resub  11637  remullem  11638  imcj  11642  imneg  11643  imadd  11644  imsub  11645  cjcj  11650  cjadd  11651  ipcnval  11653  cjmulrcl  11654  cjneg  11657  addcj  11658  cjsub  11659  sq01  11662  cnrecnv  11678  caucvgrelemcau  11748  cvg1nlemcau  11752  cvg1nlemres  11753  recvguniqlem  11762  resqrexlemover  11778  resqrexlemlo  11781  resqrexlemcalc1  11782  resqrexlemcalc3  11784  resqrexlemnm  11786  resqrexlemcvg  11787  absneg  11818  abscj  11820  sqabsadd  11823  sqabssub  11824  absmul  11837  absid  11839  absre  11845  absresq  11846  absexpzap  11848  recvalap  11865  abstri  11872  abs2dif2  11875  recan  11877  cau3lem  11882  amgm2  11886  bdtrilem  12007  xrmaxadd  12029  xrbdtri  12044  climaddc1  12097  climsubc1  12100  climcvg1nlem  12117  serf0  12120  fzf1o  12144  summodclem3  12149  summodclem2a  12150  summodc  12152  fsumsplitsn  12179  fsumm1  12185  fsumsplitsnun  12188  fsump1  12189  isummulc2  12195  fsumrev  12212  fisum0diag2  12216  fsummulc2  12217  fsumsub  12221  fsumabs  12234  telfsumo  12235  fsumparts  12239  fsumrelem  12240  fsumiun  12246  binomlem  12252  binom  12253  binom1p  12254  binom11  12255  binom1dif  12256  bcxmas  12258  isumsplit  12260  isum1p  12261  divcnv  12266  arisum2  12268  trireciplem  12269  trirecip  12270  geolim  12280  georeclim  12282  geo2sum  12283  geo2lim  12285  geoisum1c  12289  0.999...  12290  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  cvgratz  12301  mertenslem2  12305  mertensabs  12306  clim2prod  12308  prodfrecap  12315  prodfdivap  12316  prodmodclem3  12344  prodmodclem2a  12345  fprodm1  12367  fprodp1  12369  fprodunsn  12373  fprodfac  12384  fprodeq0  12386  fprodconst  12389  fprodrec  12398  fproddivap  12399  fprodsplitsn  12402  ege2le3  12440  efaddlem  12443  efsub  12450  efexp  12451  eftlub  12459  efsep  12460  effsumlt  12461  ef4p  12463  tanval3ap  12483  resinval  12484  recosval  12485  efi4p  12486  efival  12501  efmival  12502  efeul  12503  sinadd  12505  cosadd  12506  tanaddap  12508  sinsub  12509  cossub  12510  sincossq  12517  sin2t  12518  cos2t  12519  cos2tsin  12520  ef01bndlem  12525  sin01bnd  12526  cos01bnd  12527  cos12dec  12537  absef  12539  absefib  12540  efieq1re  12541  demoivreALT  12543  eirraplem  12546  dvdsexp  12630  oexpneg  12646  opeo  12666  omeo  12667  m1exp1  12670  flodddiv4  12705  flodddiv4t2lthalf  12708  bitsval  12712  bitsp1  12720  bitsinv1lem  12730  bitsinv1  12731  divgcdnnr  12755  gcdaddm  12763  gcdadd  12764  gcdid  12765  modgcd  12770  gcdmultipled  12772  dvdsgcdidd  12773  bezoutlemnewy  12775  bezoutlema  12778  bezoutlemb  12779  bezoutlemex  12780  bezoutlembz  12783  absmulgcd  12796  gcdmultiple  12799  gcdmultiplez  12800  rpmulgcd  12805  rplpwr  12806  eucalginv  12836  eucalg  12839  lcmneg  12854  lcmgcdlem  12857  lcmgcd  12858  lcmid  12860  lcm1  12861  mulgcddvds  12874  qredeq  12876  divgcdcoprmex  12882  prmind2  12900  rpexp1i  12934  pw2dvdslemn  12945  pw2dvdseulemle  12947  pw2dvdseu  12948  oddpwdclemxy  12949  oddpwdclemdvds  12950  oddpwdclemndvds  12951  oddpwdclemdc  12953  2sqpwodd  12956  nn0gcdsq  12980  phiprmpw  13002  eulerthlemrprm  13009  eulerthlema  13010  eulerthlemh  13011  eulerthlemth  13012  fermltl  13014  prmdiv  13015  hashgcdlem  13018  odzdvds  13026  vfermltl  13032  modprm0  13035  nnnn0modprm0  13036  modprmn0modprm0  13037  coprimeprodsq  13038  pythagtriplem1  13046  pythagtriplem4  13049  pythagtriplem12  13056  pythagtriplem14  13058  pythagtriplem16  13060  pythagtriplem18  13062  pythagtrip  13064  pcpremul  13074  pceu  13076  pczpre  13078  pcdiv  13083  pcqmul  13084  pcqdiv  13088  pcexp  13090  pcxqcl  13093  pczdvds  13095  pczndvds  13097  pczndvds2  13099  pcid  13105  pcneg  13106  pcdvdstr  13108  pcgcd1  13109  pcgcd  13110  pc2dvds  13111  pcaddlem  13120  pcadd  13121  pcadd2  13122  pcmpt  13124  pcmpt2  13125  fldivp1  13129  pcfac  13131  pcbc  13132  expnprm  13134  prmpwdvds  13136  pockthlem  13137  pockthi  13139  4sqlem7  13165  4sqlem9  13167  4sqlem10  13168  4sqlem2  13170  4sqlem3  13171  4sqlem4  13173  mul4sqlem  13174  4sqlem11  13182  4sqlem16  13187  4sqlem17  13188  4sqlem19  13190  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilemsv  13255  ballotfilemsima  13261  ballotfilemfrci  13273  setscomd  13395  ressvalsets  13420  strressid  13427  ressval3d  13428  ressinbasd  13430  ressressg  13431  ressabsg  13432  grpinvalem  13707  grpinva  13708  grprida  13709  isnsgrp  13723  sgrpass  13725  sgrp1  13728  sgrppropd  13730  mnd32g  13742  mnd4g  13744  mndpropd  13755  imasmnd2  13761  mhmex  13771  mhmlin  13776  gzsumwmhm  13805  grprcan  13844  grpsubval  13853  grpinvid2  13860  grpasscan2  13871  grpsubinv  13880  grpinvadd  13885  grpsubid1  13892  grpsubadd0sub  13894  grpsubadd  13895  grpsubsub  13896  grpaddsubass  13897  grppncan  13898  grpnnncan2  13904  grpsubpropd2  13912  imasgrp2  13915  mhmlem  13919  mhmid  13920  mhmmnd  13921  ghmgrp  13923  mulgnn0gzsum  13933  mulgnnp1  13935  mulgaddcomlem  13950  mulgaddcom  13951  mulginvinv  13953  mulgnn0dir  13957  mulgdirlem  13958  mulgp1  13960  mulgneg2  13961  mulgnn0ass  13963  mulgass  13964  mulgmodid  13966  mulgsubdir  13967  nmzsubg  14015  0nsg  14019  eqger  14029  qussub  14042  ghmlin  14053  ghmsub  14056  conjghm  14081  ablsub4  14119  abladdsub4  14120  ablsubsub4  14125  ablsub32  14128  ablnnncan  14129  gzsumconst  14145  gzsummhm2  14148  gzsumsnfd  14149  gzsumsplit0  14150  gsumvalfi  14154  gzsumgsum1  14155  gzsumgsum  14157  gsumsncmn  14158  gsump1  14159  gsumzfi  14160  gsumclfi  14161  gsumf1ofi  14162  gsummptfidmadd  14163  gsummptfidmadd2  14164  gsumsubmclfi  14165  gsummhm2fi  14167  gsumconstcmn  14168  prdssgrpd  14193  prdsidlem  14195  prdsmndd  14196  mgpress  14232  rngass  14240  rngdi  14241  rngdir  14242  rngrz  14247  rngmneg2  14249  rngsubdi  14252  rngsubdir  14253  rngpropd  14256  imasrng  14257  srgass  14277  srgpcomp  14296  srgpcompp  14297  srgpcomppsc  14298  srg1expzeq1  14301  ringpropd  14345  ringrz  14351  ringnegr  14359  ringmneg2  14361  ringsubdi  14363  ringsubdir  14364  ring1  14366  imasring  14371  opprrng  14384  opprring  14386  mulgass3  14393  dvdsrd  14403  unitgrp  14425  invrfvald  14431  dvr1  14447  dvrass  14448  dvrcan1  14449  dvrcan3  14450  rdivmuldivd  14453  subrginv  14547  subrgdv  14548  resrhm2b  14559  rrgsupp  14576  islmod  14629  lmodlema  14630  islmodd  14631  lmodvs0  14661  lmodvneg1  14669  lmodvsubval2  14681  lmodsubvs  14682  lmodsubdi  14683  lmodsubdir  14684  lmodprop2d  14687  rmodislmodlem  14689  rmodislmod  14690  lsssn0  14709  sraval  14776  cnfldsub  14914  gsumfsum  14925  mulgrhm  14946  mulgrhm2  14947  znval  14973  znval2  14975  znunit  14996  isassa  15004  assalem  15005  assa2ass2  15012  assapropd  15016  asclmul1  15031  asclmul2  15032  ascldimul  15033  asclpropd  15042  assamulgscmlem2  15044  asclmulg  15046  psrval  15052  mplvalcoe  15083  mplval2g  15088  restabs  15278  cnprcl2k  15309  cnrest2r  15340  ispsmet  15426  psmettri2  15431  psmetsym  15432  ismet  15447  isxmet  15448  xmettri2  15464  xmetsym  15471  xmettri3  15477  mettri3  15478  xblss2ps  15507  xblss2  15508  comet  15602  xmetxp  15610  xmetxpbl  15611  txmetcnp  15621  fsumcncntop  15670  cncfi  15681  divcncfap  15717  limccl  15762  ellimc3apf  15763  limccnpcntop  15778  limccnp2lem  15779  reldvg  15782  dvfvalap  15784  eldvap  15785  dvcj  15812  dvfre  15813  dvexp  15814  dvexp2  15815  dvrecap  15816  dvmptaddx  15822  dvmptmulx  15823  dvmptnegcn  15825  dvmptsubcn  15826  dvmptcjx  15827  dvmptfsum  15828  dveflem  15829  dvef  15830  plyconst  15848  plyaddlem1  15850  plymullem1  15851  plyadd  15854  plymul  15855  plycoeid3  15860  plycolemc  15861  plyco  15862  plycjlemc  15863  plycj  15864  plyrecj  15866  dvply1  15868  dvply2g  15869  sin0pilem1  15885  sin0pilem2  15886  efper  15911  sinperlem  15912  efimpi  15923  ptolemy  15928  tangtx  15942  abssinper  15950  cosq34lt1  15954  rpcxpef  16002  rpcxpp1  16014  rpcxpneg  16015  rpcxpsub  16016  rpmulcxp  16017  rpdivcxp  16019  cxpmul  16020  rpcxpmul2  16021  rpcxproot  16022  cxpcom  16046  rpabscxpbnd  16048  rplogbval  16053  rplogbreexp  16061  rplogbzexp  16062  rprelogbmulexp  16064  rprelogbdiv  16065  relogbexpap  16066  rplogbcxp  16071  rpcxplogb  16072  logbgcd1irr  16075  logbgcd1irraplemap  16077  binom4  16087  log2tlbndlog2  16088  log2ublem2  16090  birthdaylem2  16094  pellexlem2  16098  pellexlem3  16099  wilthlem1  16100  sgmval  16103  sgmppw  16112  1sgmprm  16114  mersenne  16117  perfectlem1  16119  perfectlem2  16120  perfect  16121  bcctr  16122  pcbcctr  16123  bcmono  16124  bcp1ctr  16126  lgslem1  16131  lgsval  16135  lgsfvalg  16136  lgsval2lem  16141  lgsval4  16151  lgsneg  16155  lgsneg1  16156  lgsmod  16157  lgsdir2  16164  lgsdirprm  16165  lgsdilem2  16167  lgsdi  16168  lgsne0  16169  lgssq2  16172  lgsdirnn0  16178  lgsdinn0  16179  gausslemma2dlem1a  16189  gausslemma2dlem1f1o  16191  gausslemma2dlem2  16193  gausslemma2dlem3  16194  gausslemma2dlem4  16195  gausslemma2dlem5  16197  gausslemma2dlem6  16198  gausslemma2d  16200  lgseisenlem1  16201  lgseisenlem2  16202  lgseisenlem3  16203  lgseisenlem4  16204  lgsquadlem1  16208  lgsquadlem2  16209  lgsquadlem3  16210  lgsquad2lem1  16212  lgsquad2lem2  16213  lgsquad2  16214  lgsquad3  16215  m1lgs  16216  2lgslem3c  16226  2lgslem3d  16227  2lgslem3d1  16231  2sqlem2  16246  2sqlem3  16248  2sqlem4  16249  2sqlem8  16254  2sqlem9  16255  2sqlem10  16256  vtxdumgrfival  16551  p1evtxdeqfi  16565  p1evtxdp1fi  16566  iswlk  16576  upgr2wlkdc  16630  wlkres  16632  trlreslem  16642  isclwwlk  16647  clwwlkccatlem  16653  clwwlknp  16670  clwwlkn1  16671  clwwlkn2  16674  clwwlkext2edg  16675  clwwlknonex2lem1  16690  clwwlknonex2lem2  16691  clwwlknonex2  16692  iseupth  16700  eupth2lem3lem6fi  16724  eupth2lem3lem4fi  16726  depindlem1  16759  qdencn  17084  trilpolemclim  17097  trilpolemcl  17098  trilpolemisumle  17099  trilpolemeq1  17101  trilpolemlt1  17102  trilpo  17104  apdifflemf  17107  apdiff  17109  iswomni0  17113  redcwlpolemeq1  17116  redcwlpo  17117  nconstwlpolem0  17125  nconstwlpolemgt0  17126  nconstwlpo  17128  neapmkv  17130