Theorem oveq2d 5934

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 5926	. 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 5918

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-rex 2478  df-v 2762  df-un 3157  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-iota 5215  df-fv 5262  df-ov 5921

This theorem is referenced by:  csbov1g  5958  caovassg  6077  caovdig  6093  caovdirg  6096  caov32d  6099  caov4d  6103  caov42d  6105  nnaass  6538  nndi  6539  nnmass  6540  nnmsucr  6541  ecovass  6698  ecoviass  6699  ecovdi  6700  ecovidi  6701  addasspig  7390  mulasspig  7392  distrpig  7393  dfplpq2  7414  mulpipq2  7431  addassnqg  7442  prarloclemarch  7478  prarloclemarch2  7479  ltrnqg  7480  enq0sym  7492  addnq0mo  7507  mulnq0mo  7508  addnnnq0  7509  nq0a0  7517  distrnq0  7519  addassnq0  7522  prarloclemlo  7554  prarloclem3  7557  prarloclem5  7560  prarloclemcalc  7562  addnqprl  7589  addnqpru  7590  prmuloclemcalc  7625  mulnqprl  7628  mulnqpru  7629  distrlem4prl  7644  distrlem4pru  7645  1idprl  7650  1idpru  7651  ltexprlemloc  7667  addcanprleml  7674  addcanprlemu  7675  recexprlem1ssu  7694  ltmprr  7702  caucvgprlemcanl  7704  cauappcvgprlemladdru  7716  cauappcvgprlemladdrl  7717  cauappcvgprlem1  7719  cauappcvgprlemlim  7721  caucvgprlemnkj  7726  caucvgprlemnbj  7727  caucvgprlemdisj  7734  caucvgprlemloc  7735  caucvgprlemcl  7736  caucvgprlemladdrl  7738  caucvgprlem1  7739  caucvgpr  7742  caucvgprprlemell  7745  caucvgprprlemcbv  7747  caucvgprprlemval  7748  caucvgprprlemnkeqj  7750  caucvgprprlemopl  7757  caucvgprprlemlol  7758  caucvgprprlemloc  7763  caucvgprprlemclphr  7765  caucvgprprlemexb  7767  caucvgprprlemaddq  7768  caucvgprprlem1  7769  addcmpblnr  7799  mulcmpblnrlemg  7800  addsrmo  7803  mulsrmo  7804  addsrpr  7805  mulsrpr  7806  ltsrprg  7807  recexgt0sr  7833  mulgt0sr  7838  caucvgsrlemgt1  7855  caucvgsrlemoffval  7856  caucvgsr  7862  suplocsrlemb  7866  suplocsrlempr  7867  suplocsrlem  7868  suplocsr  7869  mulcnsr  7895  pitoregt0  7909  recidpirqlemcalc  7917  axmulcom  7931  axmulass  7933  axdistr  7934  ax0id  7938  axcnre  7941  recriota  7950  axcaucvglemcau  7958  axcaucvglemres  7959  mulrid  8016  adddirp1d  8046  mul32  8149  mul31  8150  add32  8178  add4  8180  add42  8181  cnegex  8197  addcan2  8200  addsubass  8229  subsub2  8247  nppcan2  8250  sub32  8253  nnncan  8254  sub4  8264  muladd  8403  subdi  8404  mul2neg  8417  submul2  8418  mulsub  8420  mulsubfacd  8437  add20  8493  recexre  8597  rereim  8605  apreap  8606  ltmul1  8611  cru  8621  apreim  8622  mulreim  8623  apadd1  8627  apneg  8630  mulap0  8673  divrecap  8707  divassap  8709  divmulasscomap  8715  divsubdirap  8727  divdivdivap  8732  divmul24ap  8735  divmuleqap  8736  divcanap6  8738  divdivap1  8742  divdivap2  8743  divsubdivap  8747  conjmulap  8748  div2negap  8754  apmul1  8807  cju  8980  nnmulcl  9003  add1p1  9232  sub1m1  9233  cnm2m1cnm3  9234  xp1d2m1eqxm1d2  9235  div4p1lem1div2  9236  un0addcl  9273  un0mulcl  9274  zaddcllemneg  9356  qapne  9704  cnref1o  9716  rexsub  9919  xnegid  9925  xaddcom  9927  xnegdi  9934  xaddass  9935  xaddass2  9936  xpncan  9937  xnpcan  9938  xleadd1a  9939  xsubge0  9947  xposdif  9948  xlesubadd  9949  xadd4d  9951  lincmb01cmp  10069  iccf1o  10070  ige3m2fz  10115  fztp  10144  fzsuc2  10145  fseq1m1p1  10161  fzm1  10166  ige2m1fz1  10175  nn0split  10202  nnsplit  10203  fzval3  10271  zpnn0elfzo1  10275  fzosplitsnm1  10276  fzosplitprm1  10301  fzoshftral  10305  rebtwn2zlemstep  10321  flhalf  10371  fldiv4lem1div2uz2  10375  modqval  10395  modqvalr  10396  modqdiffl  10406  modqfrac  10408  flqmod  10409  intqfrac  10410  zmod10  10411  modqmulnn  10413  modqvalp1  10414  modqid  10420  modqcyc  10430  modqcyc2  10431  modqmul1  10448  q2submod  10456  modqdi  10463  modqsubdir  10464  modqeqmodmin  10465  modsumfzodifsn  10467  addmodlteq  10469  frecuzrdgsuctlem  10494  uzsinds  10515  seqeq3  10523  iseqvalcbv  10530  seq3val  10531  seqvalcd  10532  seqf  10535  seq3p1  10536  seqovcd  10538  seqp1cd  10541  seq3m1  10544  seq3fveq2  10546  seqfveq2g  10548  seq3shft2  10552  seqshft2g  10553  monoord2  10557  ser3mono  10558  seq3split  10559  seqsplitg  10560  seq3caopr3  10562  seqcaopr3g  10563  seq3caopr2  10564  seqcaopr2g  10565  seq3caopr  10566  seqcaoprg  10567  seqf1oglem2a  10589  seqf1oglem2  10591  seq3id2  10597  seq3homo  10598  seq3z  10599  seqhomog  10601  exp3vallem  10611  exp3val  10612  expp1  10617  expnegap0  10618  expineg2  10619  expn1ap0  10620  expm1t  10638  1exp  10639  expnegzap  10644  mulexpzap  10650  expadd  10652  expaddzaplem  10653  expaddzap  10654  expmul  10655  expmulzap  10656  m1expeven  10657  expsubap  10658  expp1zap  10659  expm1ap  10660  expdivap  10661  iexpcyc  10715  subsq2  10718  binom2  10722  binom21  10723  binom2sub  10724  binom2sub1  10725  mulbinom2  10727  binom3  10728  zesq  10729  bernneq  10731  sqoddm1div8  10764  mulsubdivbinom2ap  10782  nn0opthlem1d  10791  nn0opthd  10793  facp1  10801  facnn2  10805  faclbnd  10812  faclbnd6  10815  bcval  10820  bccmpl  10825  bcn0  10826  bcnn  10828  bcnp1n  10830  bcm1k  10831  bcp1n  10832  bcp1nk  10833  bcval5  10834  bcp1m1  10836  bcpasc  10837  bcn2m1  10840  bcn2p1  10841  omgadd  10873  hashunlem  10875  hashunsng  10878  hashdifsn  10890  hashxp  10897  zfz1isolemsplit  10909  zfz1isolem1  10911  zfz1iso  10912  seq3coll  10913  wrdf  10920  shftcan1  10978  shftcan2  10979  cjval  10989  cjth  10990  crre  11001  replim  11003  remim  11004  reim0b  11006  rereb  11007  mulreap  11008  cjreb  11010  recj  11011  reneg  11012  readd  11013  resub  11014  remullem  11015  imcj  11019  imneg  11020  imadd  11021  imsub  11022  cjcj  11027  cjadd  11028  ipcnval  11030  cjmulrcl  11031  cjneg  11034  addcj  11035  cjsub  11036  cnrecnv  11054  caucvgrelemcau  11124  cvg1nlemcau  11128  cvg1nlemres  11129  recvguniqlem  11138  resqrexlemover  11154  resqrexlemlo  11157  resqrexlemcalc1  11158  resqrexlemcalc3  11160  resqrexlemnm  11162  resqrexlemcvg  11163  absneg  11194  abscj  11196  sqabsadd  11199  sqabssub  11200  absmul  11213  absid  11215  absre  11221  absresq  11222  absexpzap  11224  recvalap  11241  abstri  11248  abs2dif2  11251  recan  11253  cau3lem  11258  amgm2  11262  bdtrilem  11382  xrmaxadd  11404  xrbdtri  11419  climaddc1  11472  climsubc1  11475  climcvg1nlem  11492  serf0  11495  summodclem3  11523  summodclem2a  11524  summodc  11526  fsumsplitsn  11553  fsumm1  11559  fsumsplitsnun  11562  fsump1  11563  isummulc2  11569  fsumrev  11586  fisum0diag2  11590  fsummulc2  11591  fsumsub  11595  fsumabs  11608  telfsumo  11609  fsumparts  11613  fsumrelem  11614  fsumiun  11620  binomlem  11626  binom  11627  binom1p  11628  binom11  11629  binom1dif  11630  bcxmas  11632  isumsplit  11634  isum1p  11635  divcnv  11640  arisum2  11642  trireciplem  11643  trirecip  11644  geolim  11654  georeclim  11656  geo2sum  11657  geo2lim  11659  geoisum1c  11663  0.999...  11664  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  cvgratz  11675  mertenslem2  11679  mertensabs  11680  clim2prod  11682  prodfrecap  11689  prodfdivap  11690  prodmodclem3  11718  prodmodclem2a  11719  fprodm1  11741  fprodp1  11743  fprodunsn  11747  fprodfac  11758  fprodeq0  11760  fprodconst  11763  fprodrec  11772  fproddivap  11773  fprodsplitsn  11776  ege2le3  11814  efaddlem  11817  efsub  11824  efexp  11825  eftlub  11833  efsep  11834  effsumlt  11835  ef4p  11837  tanval3ap  11857  resinval  11858  recosval  11859  efi4p  11860  efival  11875  efmival  11876  efeul  11877  sinadd  11879  cosadd  11880  tanaddap  11882  sinsub  11883  cossub  11884  sincossq  11891  sin2t  11892  cos2t  11893  cos2tsin  11894  ef01bndlem  11899  sin01bnd  11900  cos01bnd  11901  cos12dec  11911  absef  11913  absefib  11914  efieq1re  11915  demoivreALT  11917  eirraplem  11920  dvdsexp  12003  oexpneg  12018  opeo  12038  omeo  12039  m1exp1  12042  flodddiv4  12075  flodddiv4t2lthalf  12078  divgcdnnr  12113  gcdaddm  12121  gcdadd  12122  gcdid  12123  modgcd  12128  gcdmultipled  12130  dvdsgcdidd  12131  bezoutlemnewy  12133  bezoutlema  12136  bezoutlemb  12137  bezoutlemex  12138  bezoutlembz  12141  absmulgcd  12154  gcdmultiple  12157  gcdmultiplez  12158  rpmulgcd  12163  rplpwr  12164  eucalginv  12194  eucalg  12197  lcmneg  12212  lcmgcdlem  12215  lcmgcd  12216  lcmid  12218  lcm1  12219  mulgcddvds  12232  qredeq  12234  divgcdcoprmex  12240  prmind2  12258  rpexp1i  12292  pw2dvdslemn  12303  pw2dvdseulemle  12305  pw2dvdseu  12306  oddpwdclemxy  12307  oddpwdclemdvds  12308  oddpwdclemndvds  12309  oddpwdclemdc  12311  2sqpwodd  12314  nn0gcdsq  12338  phiprmpw  12360  eulerthlemrprm  12367  eulerthlema  12368  eulerthlemh  12369  eulerthlemth  12370  fermltl  12372  prmdiv  12373  hashgcdlem  12376  odzdvds  12383  vfermltl  12389  modprm0  12392  nnnn0modprm0  12393  modprmn0modprm0  12394  coprimeprodsq  12395  pythagtriplem1  12403  pythagtriplem4  12406  pythagtriplem12  12413  pythagtriplem14  12415  pythagtriplem16  12417  pythagtriplem18  12419  pythagtrip  12421  pcpremul  12431  pceu  12433  pczpre  12435  pcdiv  12440  pcqmul  12441  pcqdiv  12445  pcexp  12447  pcxqcl  12450  pczdvds  12452  pczndvds  12454  pczndvds2  12456  pcid  12462  pcneg  12463  pcdvdstr  12465  pcgcd1  12466  pcgcd  12467  pc2dvds  12468  pcaddlem  12477  pcadd  12478  pcadd2  12479  pcmpt  12481  pcmpt2  12482  fldivp1  12486  pcfac  12488  pcbc  12489  expnprm  12491  prmpwdvds  12493  pockthlem  12494  pockthi  12496  4sqlem7  12522  4sqlem9  12524  4sqlem10  12525  4sqlem2  12527  4sqlem3  12528  4sqlem4  12530  mul4sqlem  12531  4sqlem11  12539  4sqlem16  12544  4sqlem17  12545  4sqlem19  12547  setscomd  12659  ressvalsets  12682  strressid  12689  ressval3d  12690  ressinbasd  12692  ressressg  12693  ressabsg  12694  grpinvalem  12968  grpinva  12969  grprida  12970  isnsgrp  12989  sgrpass  12991  sgrp1  12994  sgrppropd  12996  mnd32g  13008  mnd4g  13010  mndpropd  13021  mhmex  13034  mhmlin  13039  gsumwmhm  13070  grprcan  13109  grpsubval  13118  grpinvid2  13125  grpasscan2  13136  grpsubinv  13145  grpinvadd  13150  grpsubid1  13157  grpsubadd0sub  13159  grpsubadd  13160  grpsubsub  13161  grpaddsubass  13162  grppncan  13163  grpnnncan2  13169  grpsubpropd2  13177  imasgrp2  13180  mhmlem  13184  mhmid  13185  mhmmnd  13186  ghmgrp  13188  mulgnn0gsum  13198  mulgnnp1  13200  mulgaddcomlem  13215  mulgaddcom  13216  mulginvinv  13218  mulgnn0dir  13222  mulgdirlem  13223  mulgp1  13225  mulgneg2  13226  mulgnn0ass  13228  mulgass  13229  mulgmodid  13231  mulgsubdir  13232  nmzsubg  13280  0nsg  13284  eqger  13294  qussub  13307  ghmlin  13318  ghmsub  13321  conjghm  13346  ablsub4  13383  abladdsub4  13384  ablsubsub4  13389  ablsub32  13392  ablnnncan  13393  gsumfzmptfidmadd2  13410  gsumfzconst  13411  gsumfzmhm2  13414  gsumfzsnfd  13415  mgpress  13427  rngass  13435  rngdi  13436  rngdir  13437  rngrz  13442  rngmneg2  13444  rngsubdi  13447  rngsubdir  13448  rngpropd  13451  imasrng  13452  srgass  13467  srgpcomp  13486  srgpcompp  13487  srgpcomppsc  13488  srg1expzeq1  13491  ringpropd  13534  ringrz  13540  ringnegr  13548  ringmneg2  13550  ringsubdi  13552  ringsubdir  13553  ring1  13555  imasring  13560  opprrng  13573  opprring  13575  mulgass3  13581  dvdsrd  13590  unitgrp  13612  invrfvald  13618  dvr1  13634  dvrass  13635  dvrcan1  13636  dvrcan3  13637  rdivmuldivd  13640  subrginv  13733  subrgdv  13734  resrhm2b  13745  islmod  13787  lmodlema  13788  islmodd  13789  lmodvs0  13818  lmodvneg1  13826  lmodvsubval2  13838  lmodsubvs  13839  lmodsubdi  13840  lmodsubdir  13841  lmodprop2d  13844  rmodislmodlem  13846  rmodislmod  13847  lsssn0  13866  sraval  13933  cnfldsub  14063  gsumfzfsumlem0  14074  gsumfzfsumlemm  14075  mulgrhm  14097  mulgrhm2  14098  znval  14124  znval2  14126  znunit  14147  psrval  14152  restabs  14343  cnprcl2k  14374  cnrest2r  14405  ispsmet  14491  psmettri2  14496  psmetsym  14497  ismet  14512  isxmet  14513  xmettri2  14529  xmetsym  14536  xmettri3  14542  mettri3  14543  xblss2ps  14572  xblss2  14573  comet  14667  xmetxp  14675  xmetxpbl  14676  txmetcnp  14686  fsumcncntop  14724  cncfi  14733  divcncfap  14768  limccl  14813  ellimc3apf  14814  limccnpcntop  14829  limccnp2lem  14830  reldvg  14833  dvfvalap  14835  eldvap  14836  dvcj  14858  dvfre  14859  dvexp  14860  dvexp2  14861  dvrecap  14862  dvmptaddx  14866  dvmptmulx  14867  dvmptnegcn  14869  dvmptsubcn  14870  dvmptcjx  14871  dveflem  14872  dvef  14873  plyconst  14891  plyaddlem1  14893  plymullem1  14894  plyadd  14897  plymul  14898  sin0pilem1  14916  sin0pilem2  14917  efper  14942  sinperlem  14943  efimpi  14954  ptolemy  14959  tangtx  14973  abssinper  14981  cosq34lt1  14985  rpcxpef  15029  rpcxpp1  15041  rpcxpneg  15042  rpcxpsub  15043  rpmulcxp  15044  rpdivcxp  15046  cxpmul  15047  rpcxproot  15048  cxpcom  15071  rpabscxpbnd  15073  rplogbval  15077  rplogbreexp  15085  rplogbzexp  15086  rprelogbmulexp  15088  rprelogbdiv  15089  relogbexpap  15090  rplogbcxp  15095  rpcxplogb  15096  logbgcd1irr  15099  logbgcd1irraplemap  15101  binom4  15111  wilthlem1  15112  lgslem1  15116  lgsval  15120  lgsfvalg  15121  lgsval2lem  15126  lgsval4  15136  lgsneg  15140  lgsneg1  15141  lgsmod  15142  lgsdir2  15149  lgsdirprm  15150  lgsdilem2  15152  lgsdi  15153  lgsne0  15154  lgssq2  15157  lgsdirnn0  15163  lgsdinn0  15164  gausslemma2dlem1a  15174  gausslemma2dlem1f1o  15176  gausslemma2dlem2  15178  gausslemma2dlem3  15179  gausslemma2dlem4  15180  gausslemma2dlem5  15182  gausslemma2dlem6  15183  gausslemma2d  15185  lgseisenlem1  15186  lgseisenlem2  15187  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  m1lgs  15192  2sqlem2  15202  2sqlem3  15204  2sqlem4  15205  2sqlem8  15210  2sqlem9  15211  2sqlem10  15212  qdencn  15517  trilpolemclim  15526  trilpolemcl  15527  trilpolemisumle  15528  trilpolemeq1  15530  trilpolemlt1  15531  trilpo  15533  apdifflemf  15536  apdiff  15538  iswomni0  15541  redcwlpolemeq1  15544  redcwlpo  15545  nconstwlpolem0  15553  nconstwlpolemgt0  15554  nconstwlpo  15556  neapmkv  15558