Theorem oveq2d 5938

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 5930	. 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 1364  (class class class)co 5922

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925

This theorem is referenced by:  csbov1g  5962  caovassg  6082  caovdig  6098  caovdirg  6101  caov32d  6104  caov4d  6108  caov42d  6110  nnaass  6543  nndi  6544  nnmass  6545  nnmsucr  6546  ecovass  6703  ecoviass  6704  ecovdi  6705  ecovidi  6706  addasspig  7397  mulasspig  7399  distrpig  7400  dfplpq2  7421  mulpipq2  7438  addassnqg  7449  prarloclemarch  7485  prarloclemarch2  7486  ltrnqg  7487  enq0sym  7499  addnq0mo  7514  mulnq0mo  7515  addnnnq0  7516  nq0a0  7524  distrnq0  7526  addassnq0  7529  prarloclemlo  7561  prarloclem3  7564  prarloclem5  7567  prarloclemcalc  7569  addnqprl  7596  addnqpru  7597  prmuloclemcalc  7632  mulnqprl  7635  mulnqpru  7636  distrlem4prl  7651  distrlem4pru  7652  1idprl  7657  1idpru  7658  ltexprlemloc  7674  addcanprleml  7681  addcanprlemu  7682  recexprlem1ssu  7701  ltmprr  7709  caucvgprlemcanl  7711  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  cauappcvgprlem1  7726  cauappcvgprlemlim  7728  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemdisj  7741  caucvgprlemloc  7742  caucvgprlemcl  7743  caucvgprlemladdrl  7745  caucvgprlem1  7746  caucvgpr  7749  caucvgprprlemell  7752  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemnkeqj  7757  caucvgprprlemopl  7764  caucvgprprlemlol  7765  caucvgprprlemloc  7770  caucvgprprlemclphr  7772  caucvgprprlemexb  7774  caucvgprprlemaddq  7775  caucvgprprlem1  7776  addcmpblnr  7806  mulcmpblnrlemg  7807  addsrmo  7810  mulsrmo  7811  addsrpr  7812  mulsrpr  7813  ltsrprg  7814  recexgt0sr  7840  mulgt0sr  7845  caucvgsrlemgt1  7862  caucvgsrlemoffval  7863  caucvgsr  7869  suplocsrlemb  7873  suplocsrlempr  7874  suplocsrlem  7875  suplocsr  7876  mulcnsr  7902  pitoregt0  7916  recidpirqlemcalc  7924  axmulcom  7938  axmulass  7940  axdistr  7941  ax0id  7945  axcnre  7948  recriota  7957  axcaucvglemcau  7965  axcaucvglemres  7966  mulrid  8023  adddirp1d  8053  mul32  8156  mul31  8157  add32  8185  add4  8187  add42  8188  cnegex  8204  addcan2  8207  addsubass  8236  subsub2  8254  nppcan2  8257  sub32  8260  nnncan  8261  sub4  8271  muladd  8410  subdi  8411  mul2neg  8424  submul2  8425  mulsub  8427  muls1d  8444  mulsubfacd  8445  add20  8501  recexre  8605  rereim  8613  apreap  8614  ltmul1  8619  cru  8629  apreim  8630  mulreim  8631  apadd1  8635  apneg  8638  mulap0  8681  divrecap  8715  divassap  8717  divmulasscomap  8723  divsubdirap  8735  divdivdivap  8740  divmul24ap  8743  divmuleqap  8744  divcanap6  8746  divdivap1  8750  divdivap2  8751  divsubdivap  8755  conjmulap  8756  div2negap  8762  apmul1  8815  cju  8988  nnmulcl  9011  add1p1  9241  sub1m1  9242  cnm2m1cnm3  9243  xp1d2m1eqxm1d2  9244  div4p1lem1div2  9245  un0addcl  9282  un0mulcl  9283  zaddcllemneg  9365  qapne  9713  cnref1o  9725  rexsub  9928  xnegid  9934  xaddcom  9936  xnegdi  9943  xaddass  9944  xaddass2  9945  xpncan  9946  xnpcan  9947  xleadd1a  9948  xsubge0  9956  xposdif  9957  xlesubadd  9958  xadd4d  9960  lincmb01cmp  10078  iccf1o  10079  ige3m2fz  10124  fztp  10153  fzsuc2  10154  fseq1m1p1  10170  fzm1  10175  ige2m1fz1  10184  nn0split  10211  nnsplit  10212  fzval3  10280  zpnn0elfzo1  10284  fzosplitsnm1  10285  fzosplitprm1  10310  fzoshftral  10314  rebtwn2zlemstep  10342  flhalf  10392  fldiv4lem1div2uz2  10396  modqval  10416  modqvalr  10417  modqdiffl  10427  modqfrac  10429  flqmod  10430  intqfrac  10431  zmod10  10432  modqmulnn  10434  modqvalp1  10435  modqid  10441  modqcyc  10451  modqcyc2  10452  modqmul1  10469  q2submod  10477  modqdi  10484  modqsubdir  10485  modqeqmodmin  10486  modsumfzodifsn  10488  addmodlteq  10490  frecuzrdgsuctlem  10515  uzsinds  10536  seqeq3  10544  iseqvalcbv  10551  seq3val  10552  seqvalcd  10553  seqf  10556  seq3p1  10557  seqovcd  10559  seqp1cd  10562  seq3m1  10565  seq3fveq2  10567  seqfveq2g  10569  seq3shft2  10573  seqshft2g  10574  monoord2  10578  ser3mono  10579  seq3split  10580  seqsplitg  10581  seq3caopr3  10583  seqcaopr3g  10584  seq3caopr2  10585  seqcaopr2g  10586  seq3caopr  10587  seqcaoprg  10588  seqf1oglem2a  10610  seqf1oglem2  10612  seq3id2  10618  seq3homo  10619  seq3z  10620  seqhomog  10622  exp3vallem  10632  exp3val  10633  expp1  10638  expnegap0  10639  expineg2  10640  expn1ap0  10641  expm1t  10659  1exp  10660  expnegzap  10665  mulexpzap  10671  expadd  10673  expaddzaplem  10674  expaddzap  10675  expmul  10676  expmulzap  10677  m1expeven  10678  expsubap  10679  expp1zap  10680  expm1ap  10681  expdivap  10682  iexpcyc  10736  subsq2  10739  binom2  10743  binom21  10744  binom2sub  10745  binom2sub1  10746  mulbinom2  10748  binom3  10749  zesq  10750  bernneq  10752  sqoddm1div8  10785  mulsubdivbinom2ap  10803  nn0opthlem1d  10812  nn0opthd  10814  facp1  10822  facnn2  10826  faclbnd  10833  faclbnd6  10836  bcval  10841  bccmpl  10846  bcn0  10847  bcnn  10849  bcnp1n  10851  bcm1k  10852  bcp1n  10853  bcp1nk  10854  bcval5  10855  bcp1m1  10857  bcpasc  10858  bcn2m1  10861  bcn2p1  10862  omgadd  10894  hashunlem  10896  hashunsng  10899  hashdifsn  10911  hashxp  10918  zfz1isolemsplit  10930  zfz1isolem1  10932  zfz1iso  10933  seq3coll  10934  wrdf  10941  shftcan1  10999  shftcan2  11000  cjval  11010  cjth  11011  crre  11022  replim  11024  remim  11025  reim0b  11027  rereb  11028  mulreap  11029  cjreb  11031  recj  11032  reneg  11033  readd  11034  resub  11035  remullem  11036  imcj  11040  imneg  11041  imadd  11042  imsub  11043  cjcj  11048  cjadd  11049  ipcnval  11051  cjmulrcl  11052  cjneg  11055  addcj  11056  cjsub  11057  cnrecnv  11075  caucvgrelemcau  11145  cvg1nlemcau  11149  cvg1nlemres  11150  recvguniqlem  11159  resqrexlemover  11175  resqrexlemlo  11178  resqrexlemcalc1  11179  resqrexlemcalc3  11181  resqrexlemnm  11183  resqrexlemcvg  11184  absneg  11215  abscj  11217  sqabsadd  11220  sqabssub  11221  absmul  11234  absid  11236  absre  11242  absresq  11243  absexpzap  11245  recvalap  11262  abstri  11269  abs2dif2  11272  recan  11274  cau3lem  11279  amgm2  11283  bdtrilem  11404  xrmaxadd  11426  xrbdtri  11441  climaddc1  11494  climsubc1  11497  climcvg1nlem  11514  serf0  11517  summodclem3  11545  summodclem2a  11546  summodc  11548  fsumsplitsn  11575  fsumm1  11581  fsumsplitsnun  11584  fsump1  11585  isummulc2  11591  fsumrev  11608  fisum0diag2  11612  fsummulc2  11613  fsumsub  11617  fsumabs  11630  telfsumo  11631  fsumparts  11635  fsumrelem  11636  fsumiun  11642  binomlem  11648  binom  11649  binom1p  11650  binom11  11651  binom1dif  11652  bcxmas  11654  isumsplit  11656  isum1p  11657  divcnv  11662  arisum2  11664  trireciplem  11665  trirecip  11666  geolim  11676  georeclim  11678  geo2sum  11679  geo2lim  11681  geoisum1c  11685  0.999...  11686  cvgratnnlemnexp  11689  cvgratnnlemmn  11690  cvgratz  11697  mertenslem2  11701  mertensabs  11702  clim2prod  11704  prodfrecap  11711  prodfdivap  11712  prodmodclem3  11740  prodmodclem2a  11741  fprodm1  11763  fprodp1  11765  fprodunsn  11769  fprodfac  11780  fprodeq0  11782  fprodconst  11785  fprodrec  11794  fproddivap  11795  fprodsplitsn  11798  ege2le3  11836  efaddlem  11839  efsub  11846  efexp  11847  eftlub  11855  efsep  11856  effsumlt  11857  ef4p  11859  tanval3ap  11879  resinval  11880  recosval  11881  efi4p  11882  efival  11897  efmival  11898  efeul  11899  sinadd  11901  cosadd  11902  tanaddap  11904  sinsub  11905  cossub  11906  sincossq  11913  sin2t  11914  cos2t  11915  cos2tsin  11916  ef01bndlem  11921  sin01bnd  11922  cos01bnd  11923  cos12dec  11933  absef  11935  absefib  11936  efieq1re  11937  demoivreALT  11939  eirraplem  11942  dvdsexp  12026  oexpneg  12042  opeo  12062  omeo  12063  m1exp1  12066  flodddiv4  12101  flodddiv4t2lthalf  12104  bitsval  12108  bitsp1  12115  divgcdnnr  12143  gcdaddm  12151  gcdadd  12152  gcdid  12153  modgcd  12158  gcdmultipled  12160  dvdsgcdidd  12161  bezoutlemnewy  12163  bezoutlema  12166  bezoutlemb  12167  bezoutlemex  12168  bezoutlembz  12171  absmulgcd  12184  gcdmultiple  12187  gcdmultiplez  12188  rpmulgcd  12193  rplpwr  12194  eucalginv  12224  eucalg  12227  lcmneg  12242  lcmgcdlem  12245  lcmgcd  12246  lcmid  12248  lcm1  12249  mulgcddvds  12262  qredeq  12264  divgcdcoprmex  12270  prmind2  12288  rpexp1i  12322  pw2dvdslemn  12333  pw2dvdseulemle  12335  pw2dvdseu  12336  oddpwdclemxy  12337  oddpwdclemdvds  12338  oddpwdclemndvds  12339  oddpwdclemdc  12341  2sqpwodd  12344  nn0gcdsq  12368  phiprmpw  12390  eulerthlemrprm  12397  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  fermltl  12402  prmdiv  12403  hashgcdlem  12406  odzdvds  12414  vfermltl  12420  modprm0  12423  nnnn0modprm0  12424  modprmn0modprm0  12425  coprimeprodsq  12426  pythagtriplem1  12434  pythagtriplem4  12437  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem16  12448  pythagtriplem18  12450  pythagtrip  12452  pcpremul  12462  pceu  12464  pczpre  12466  pcdiv  12471  pcqmul  12472  pcqdiv  12476  pcexp  12478  pcxqcl  12481  pczdvds  12483  pczndvds  12485  pczndvds2  12487  pcid  12493  pcneg  12494  pcdvdstr  12496  pcgcd1  12497  pcgcd  12498  pc2dvds  12499  pcaddlem  12508  pcadd  12509  pcadd2  12510  pcmpt  12512  pcmpt2  12513  fldivp1  12517  pcfac  12519  pcbc  12520  expnprm  12522  prmpwdvds  12524  pockthlem  12525  pockthi  12527  4sqlem7  12553  4sqlem9  12555  4sqlem10  12556  4sqlem2  12558  4sqlem3  12559  4sqlem4  12561  mul4sqlem  12562  4sqlem11  12570  4sqlem16  12575  4sqlem17  12576  4sqlem19  12578  setscomd  12719  ressvalsets  12742  strressid  12749  ressval3d  12750  ressinbasd  12752  ressressg  12753  ressabsg  12754  grpinvalem  13028  grpinva  13029  grprida  13030  isnsgrp  13049  sgrpass  13051  sgrp1  13054  sgrppropd  13056  mnd32g  13068  mnd4g  13070  mndpropd  13081  mhmex  13094  mhmlin  13099  gsumwmhm  13130  grprcan  13169  grpsubval  13178  grpinvid2  13185  grpasscan2  13196  grpsubinv  13205  grpinvadd  13210  grpsubid1  13217  grpsubadd0sub  13219  grpsubadd  13220  grpsubsub  13221  grpaddsubass  13222  grppncan  13223  grpnnncan2  13229  grpsubpropd2  13237  imasgrp2  13240  mhmlem  13244  mhmid  13245  mhmmnd  13246  ghmgrp  13248  mulgnn0gsum  13258  mulgnnp1  13260  mulgaddcomlem  13275  mulgaddcom  13276  mulginvinv  13278  mulgnn0dir  13282  mulgdirlem  13283  mulgp1  13285  mulgneg2  13286  mulgnn0ass  13288  mulgass  13289  mulgmodid  13291  mulgsubdir  13292  nmzsubg  13340  0nsg  13344  eqger  13354  qussub  13367  ghmlin  13378  ghmsub  13381  conjghm  13406  ablsub4  13443  abladdsub4  13444  ablsubsub4  13449  ablsub32  13452  ablnnncan  13453  gsumfzmptfidmadd2  13470  gsumfzconst  13471  gsumfzmhm2  13474  gsumfzsnfd  13475  mgpress  13487  rngass  13495  rngdi  13496  rngdir  13497  rngrz  13502  rngmneg2  13504  rngsubdi  13507  rngsubdir  13508  rngpropd  13511  imasrng  13512  srgass  13527  srgpcomp  13546  srgpcompp  13547  srgpcomppsc  13548  srg1expzeq1  13551  ringpropd  13594  ringrz  13600  ringnegr  13608  ringmneg2  13610  ringsubdi  13612  ringsubdir  13613  ring1  13615  imasring  13620  opprrng  13633  opprring  13635  mulgass3  13641  dvdsrd  13650  unitgrp  13672  invrfvald  13678  dvr1  13694  dvrass  13695  dvrcan1  13696  dvrcan3  13697  rdivmuldivd  13700  subrginv  13793  subrgdv  13794  resrhm2b  13805  islmod  13847  lmodlema  13848  islmodd  13849  lmodvs0  13878  lmodvneg1  13886  lmodvsubval2  13898  lmodsubvs  13899  lmodsubdi  13900  lmodsubdir  13901  lmodprop2d  13904  rmodislmodlem  13906  rmodislmod  13907  lsssn0  13926  sraval  13993  cnfldsub  14131  gsumfzfsumlem0  14142  gsumfzfsumlemm  14143  mulgrhm  14165  mulgrhm2  14166  znval  14192  znval2  14194  znunit  14215  psrval  14220  restabs  14411  cnprcl2k  14442  cnrest2r  14473  ispsmet  14559  psmettri2  14564  psmetsym  14565  ismet  14580  isxmet  14581  xmettri2  14597  xmetsym  14604  xmettri3  14610  mettri3  14611  xblss2ps  14640  xblss2  14641  comet  14735  xmetxp  14743  xmetxpbl  14744  txmetcnp  14754  fsumcncntop  14803  cncfi  14814  divcncfap  14850  limccl  14895  ellimc3apf  14896  limccnpcntop  14911  limccnp2lem  14912  reldvg  14915  dvfvalap  14917  eldvap  14918  dvcj  14945  dvfre  14946  dvexp  14947  dvexp2  14948  dvrecap  14949  dvmptaddx  14955  dvmptmulx  14956  dvmptnegcn  14958  dvmptsubcn  14959  dvmptcjx  14960  dvmptfsum  14961  dveflem  14962  dvef  14963  plyconst  14981  plyaddlem1  14983  plymullem1  14984  plyadd  14987  plymul  14988  plycoeid3  14993  plycolemc  14994  plyco  14995  plycjlemc  14996  plycj  14997  plyrecj  14999  dvply1  15001  dvply2g  15002  sin0pilem1  15017  sin0pilem2  15018  efper  15043  sinperlem  15044  efimpi  15055  ptolemy  15060  tangtx  15074  abssinper  15082  cosq34lt1  15086  rpcxpef  15130  rpcxpp1  15142  rpcxpneg  15143  rpcxpsub  15144  rpmulcxp  15145  rpdivcxp  15147  cxpmul  15148  rpcxpmul2  15149  rpcxproot  15150  cxpcom  15174  rpabscxpbnd  15176  rplogbval  15181  rplogbreexp  15189  rplogbzexp  15190  rprelogbmulexp  15192  rprelogbdiv  15193  relogbexpap  15194  rplogbcxp  15199  rpcxplogb  15200  logbgcd1irr  15203  logbgcd1irraplemap  15205  binom4  15215  wilthlem1  15216  sgmval  15219  sgmppw  15228  1sgmprm  15230  mersenne  15233  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgslem1  15241  lgsval  15245  lgsfvalg  15246  lgsval2lem  15251  lgsval4  15261  lgsneg  15265  lgsneg1  15266  lgsmod  15267  lgsdir2  15274  lgsdirprm  15275  lgsdilem2  15277  lgsdi  15278  lgsne0  15279  lgssq2  15282  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem1a  15299  gausslemma2dlem1f1o  15301  gausslemma2dlem2  15303  gausslemma2dlem3  15304  gausslemma2dlem4  15305  gausslemma2dlem5  15307  gausslemma2dlem6  15308  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgsquadlem1  15318  lgsquadlem2  15319  lgsquadlem3  15320  lgsquad2lem1  15322  lgsquad2lem2  15323  lgsquad2  15324  lgsquad3  15325  m1lgs  15326  2lgslem3c  15336  2lgslem3d  15337  2lgslem3d1  15341  2sqlem2  15356  2sqlem3  15358  2sqlem4  15359  2sqlem8  15364  2sqlem9  15365  2sqlem10  15366  qdencn  15671  trilpolemclim  15680  trilpolemcl  15681  trilpolemisumle  15682  trilpolemeq1  15684  trilpolemlt1  15685  trilpo  15687  apdifflemf  15690  apdiff  15692  iswomni0  15695  redcwlpolemeq1  15698  redcwlpo  15699  nconstwlpolem0  15707  nconstwlpolemgt0  15708  nconstwlpo  15710  neapmkv  15712