Theorem oveq2d 5891

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 5883	. 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 1353  (class class class)co 5875

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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-rex 2461  df-v 2740  df-un 3134  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-br 4005  df-iota 5179  df-fv 5225  df-ov 5878

This theorem is referenced by:  csbov1g  5915  caovassg  6033  caovdig  6049  caovdirg  6052  caov32d  6055  caov4d  6059  caov42d  6061  nnaass  6486  nndi  6487  nnmass  6488  nnmsucr  6489  ecovass  6644  ecoviass  6645  ecovdi  6646  ecovidi  6647  addasspig  7329  mulasspig  7331  distrpig  7332  dfplpq2  7353  mulpipq2  7370  addassnqg  7381  prarloclemarch  7417  prarloclemarch2  7418  ltrnqg  7419  enq0sym  7431  addnq0mo  7446  mulnq0mo  7447  addnnnq0  7448  nq0a0  7456  distrnq0  7458  addassnq0  7461  prarloclemlo  7493  prarloclem3  7496  prarloclem5  7499  prarloclemcalc  7501  addnqprl  7528  addnqpru  7529  prmuloclemcalc  7564  mulnqprl  7567  mulnqpru  7568  distrlem4prl  7583  distrlem4pru  7584  1idprl  7589  1idpru  7590  ltexprlemloc  7606  addcanprleml  7613  addcanprlemu  7614  recexprlem1ssu  7633  ltmprr  7641  caucvgprlemcanl  7643  cauappcvgprlemladdru  7655  cauappcvgprlemladdrl  7656  cauappcvgprlem1  7658  cauappcvgprlemlim  7660  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemdisj  7673  caucvgprlemloc  7674  caucvgprlemcl  7675  caucvgprlemladdrl  7677  caucvgprlem1  7678  caucvgpr  7681  caucvgprprlemell  7684  caucvgprprlemcbv  7686  caucvgprprlemval  7687  caucvgprprlemnkeqj  7689  caucvgprprlemopl  7696  caucvgprprlemlol  7697  caucvgprprlemloc  7702  caucvgprprlemclphr  7704  caucvgprprlemexb  7706  caucvgprprlemaddq  7707  caucvgprprlem1  7708  addcmpblnr  7738  mulcmpblnrlemg  7739  addsrmo  7742  mulsrmo  7743  addsrpr  7744  mulsrpr  7745  ltsrprg  7746  recexgt0sr  7772  mulgt0sr  7777  caucvgsrlemgt1  7794  caucvgsrlemoffval  7795  caucvgsr  7801  suplocsrlemb  7805  suplocsrlempr  7806  suplocsrlem  7807  suplocsr  7808  mulcnsr  7834  pitoregt0  7848  recidpirqlemcalc  7856  axmulcom  7870  axmulass  7872  axdistr  7873  ax0id  7877  axcnre  7880  recriota  7889  axcaucvglemcau  7897  axcaucvglemres  7898  mulrid  7954  adddirp1d  7984  mul32  8087  mul31  8088  add32  8116  add4  8118  add42  8119  cnegex  8135  addcan2  8138  addsubass  8167  subsub2  8185  nppcan2  8188  sub32  8191  nnncan  8192  sub4  8202  muladd  8341  subdi  8342  mul2neg  8355  submul2  8356  mulsub  8358  mulsubfacd  8375  add20  8431  recexre  8535  rereim  8543  apreap  8544  ltmul1  8549  cru  8559  apreim  8560  mulreim  8561  apadd1  8565  apneg  8568  mulap0  8611  divrecap  8645  divassap  8647  divmulasscomap  8653  divsubdirap  8665  divdivdivap  8670  divmul24ap  8673  divmuleqap  8674  divcanap6  8676  divdivap1  8680  divdivap2  8681  divsubdivap  8685  conjmulap  8686  div2negap  8692  apmul1  8745  cju  8918  nnmulcl  8940  add1p1  9168  sub1m1  9169  cnm2m1cnm3  9170  xp1d2m1eqxm1d2  9171  div4p1lem1div2  9172  un0addcl  9209  un0mulcl  9210  zaddcllemneg  9292  qapne  9639  cnref1o  9650  rexsub  9853  xnegid  9859  xaddcom  9861  xnegdi  9868  xaddass  9869  xaddass2  9870  xpncan  9871  xnpcan  9872  xleadd1a  9873  xsubge0  9881  xposdif  9882  xlesubadd  9883  xadd4d  9885  lincmb01cmp  10003  iccf1o  10004  ige3m2fz  10049  fztp  10078  fzsuc2  10079  fseq1m1p1  10095  fzm1  10100  ige2m1fz1  10109  nn0split  10136  nnsplit  10137  fzval3  10204  zpnn0elfzo1  10208  fzosplitsnm1  10209  fzosplitprm1  10234  fzoshftral  10238  rebtwn2zlemstep  10253  flhalf  10302  modqval  10324  modqvalr  10325  modqdiffl  10335  modqfrac  10337  flqmod  10338  intqfrac  10339  zmod10  10340  modqmulnn  10342  modqvalp1  10343  modqid  10349  modqcyc  10359  modqcyc2  10360  modqmul1  10377  q2submod  10385  modqdi  10392  modqsubdir  10393  modqeqmodmin  10394  modsumfzodifsn  10396  addmodlteq  10398  frecuzrdgsuctlem  10423  uzsinds  10442  seqeq3  10450  iseqvalcbv  10457  seq3val  10458  seqvalcd  10459  seqf  10461  seq3p1  10462  seqovcd  10463  seqp1cd  10466  seq3m1  10468  seq3fveq2  10469  seq3shft2  10473  monoord2  10477  ser3mono  10478  seq3split  10479  seq3caopr3  10481  seq3caopr2  10482  seq3caopr  10483  seq3id2  10509  seq3homo  10510  seq3z  10511  exp3vallem  10521  exp3val  10522  expp1  10527  expnegap0  10528  expineg2  10529  expn1ap0  10530  expm1t  10548  1exp  10549  expnegzap  10554  mulexpzap  10560  expadd  10562  expaddzaplem  10563  expaddzap  10564  expmul  10565  expmulzap  10566  m1expeven  10567  expsubap  10568  expp1zap  10569  expm1ap  10570  expdivap  10571  iexpcyc  10625  subsq2  10628  binom2  10632  binom21  10633  binom2sub  10634  binom2sub1  10635  mulbinom2  10637  binom3  10638  zesq  10639  bernneq  10641  sqoddm1div8  10674  mulsubdivbinom2ap  10691  nn0opthlem1d  10700  nn0opthd  10702  facp1  10710  facnn2  10714  faclbnd  10721  faclbnd6  10724  bcval  10729  bccmpl  10734  bcn0  10735  bcnn  10737  bcnp1n  10739  bcm1k  10740  bcp1n  10741  bcp1nk  10742  bcval5  10743  bcp1m1  10745  bcpasc  10746  bcn2m1  10749  bcn2p1  10750  omgadd  10782  hashunlem  10784  hashunsng  10787  hashdifsn  10799  hashxp  10806  zfz1isolemsplit  10818  zfz1isolem1  10820  zfz1iso  10821  seq3coll  10822  shftcan1  10843  shftcan2  10844  cjval  10854  cjth  10855  crre  10866  replim  10868  remim  10869  reim0b  10871  rereb  10872  mulreap  10873  cjreb  10875  recj  10876  reneg  10877  readd  10878  resub  10879  remullem  10880  imcj  10884  imneg  10885  imadd  10886  imsub  10887  cjcj  10892  cjadd  10893  ipcnval  10895  cjmulrcl  10896  cjneg  10899  addcj  10900  cjsub  10901  cnrecnv  10919  caucvgrelemcau  10989  cvg1nlemcau  10993  cvg1nlemres  10994  recvguniqlem  11003  resqrexlemover  11019  resqrexlemlo  11022  resqrexlemcalc1  11023  resqrexlemcalc3  11025  resqrexlemnm  11027  resqrexlemcvg  11028  absneg  11059  abscj  11061  sqabsadd  11064  sqabssub  11065  absmul  11078  absid  11080  absre  11086  absresq  11087  absexpzap  11089  recvalap  11106  abstri  11113  abs2dif2  11116  recan  11118  cau3lem  11123  amgm2  11127  bdtrilem  11247  xrmaxadd  11269  xrbdtri  11284  climaddc1  11337  climsubc1  11340  climcvg1nlem  11357  serf0  11360  summodclem3  11388  summodclem2a  11389  summodc  11391  fsumsplitsn  11418  fsumm1  11424  fsumsplitsnun  11427  fsump1  11428  isummulc2  11434  fsumrev  11451  fisum0diag2  11455  fsummulc2  11456  fsumsub  11460  fsumabs  11473  telfsumo  11474  fsumparts  11478  fsumrelem  11479  fsumiun  11485  binomlem  11491  binom  11492  binom1p  11493  binom11  11494  binom1dif  11495  bcxmas  11497  isumsplit  11499  isum1p  11500  divcnv  11505  arisum2  11507  trireciplem  11508  trirecip  11509  geolim  11519  georeclim  11521  geo2sum  11522  geo2lim  11524  geoisum1c  11528  0.999...  11529  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  cvgratz  11540  mertenslem2  11544  mertensabs  11545  clim2prod  11547  prodfrecap  11554  prodfdivap  11555  prodmodclem3  11583  prodmodclem2a  11584  fprodm1  11606  fprodp1  11608  fprodunsn  11612  fprodfac  11623  fprodeq0  11625  fprodconst  11628  fprodrec  11637  fproddivap  11638  fprodsplitsn  11641  ege2le3  11679  efaddlem  11682  efsub  11689  efexp  11690  eftlub  11698  efsep  11699  effsumlt  11700  ef4p  11702  tanval3ap  11722  resinval  11723  recosval  11724  efi4p  11725  efival  11740  efmival  11741  efeul  11742  sinadd  11744  cosadd  11745  tanaddap  11747  sinsub  11748  cossub  11749  sincossq  11756  sin2t  11757  cos2t  11758  cos2tsin  11759  ef01bndlem  11764  sin01bnd  11765  cos01bnd  11766  cos12dec  11775  absef  11777  absefib  11778  efieq1re  11779  demoivreALT  11781  eirraplem  11784  dvdsexp  11867  oexpneg  11882  opeo  11902  omeo  11903  m1exp1  11906  flodddiv4  11939  flodddiv4t2lthalf  11942  divgcdnnr  11977  gcdaddm  11985  gcdadd  11986  gcdid  11987  modgcd  11992  gcdmultipled  11994  dvdsgcdidd  11995  bezoutlemnewy  11997  bezoutlema  12000  bezoutlemb  12001  bezoutlemex  12002  bezoutlembz  12005  absmulgcd  12018  gcdmultiple  12021  gcdmultiplez  12022  rpmulgcd  12027  rplpwr  12028  eucalginv  12056  eucalg  12059  lcmneg  12074  lcmgcdlem  12077  lcmgcd  12078  lcmid  12080  lcm1  12081  mulgcddvds  12094  qredeq  12096  divgcdcoprmex  12102  prmind2  12120  rpexp1i  12154  pw2dvdslemn  12165  pw2dvdseulemle  12167  pw2dvdseu  12168  oddpwdclemxy  12169  oddpwdclemdvds  12170  oddpwdclemndvds  12171  oddpwdclemdc  12173  2sqpwodd  12176  nn0gcdsq  12200  phiprmpw  12222  eulerthlemrprm  12229  eulerthlema  12230  eulerthlemh  12231  eulerthlemth  12232  fermltl  12234  prmdiv  12235  hashgcdlem  12238  odzdvds  12245  vfermltl  12251  modprm0  12254  nnnn0modprm0  12255  modprmn0modprm0  12256  coprimeprodsq  12257  pythagtriplem1  12265  pythagtriplem4  12268  pythagtriplem12  12275  pythagtriplem14  12277  pythagtriplem16  12279  pythagtriplem18  12281  pythagtrip  12283  pcpremul  12293  pceu  12295  pczpre  12297  pcdiv  12302  pcqmul  12303  pcqdiv  12307  pcexp  12309  pczdvds  12313  pczndvds  12315  pczndvds2  12317  pcid  12323  pcneg  12324  pcdvdstr  12326  pcgcd1  12327  pcgcd  12328  pc2dvds  12329  pcaddlem  12338  pcadd  12339  pcmpt  12341  pcmpt2  12342  fldivp1  12346  pcfac  12348  pcbc  12349  expnprm  12351  prmpwdvds  12353  pockthlem  12354  pockthi  12356  4sqlem7  12382  4sqlem9  12384  4sqlem10  12385  4sqlem2  12387  4sqlem3  12388  4sqlem4  12390  mul4sqlem  12391  setscomd  12503  ressvalsets  12524  strressid  12530  ressval3d  12531  ressinbasd  12533  ressressg  12534  ressabsg  12535  grprinvlem  12804  grprinvd  12805  grpridd  12806  isnsgrp  12812  sgrpass  12814  sgrp1  12816  mnd32g  12828  mnd4g  12830  mndpropd  12841  mhmlin  12858  grprcan  12910  grpsubval  12919  grpinvid2  12925  grpasscan2  12934  grpsubinv  12943  grpinvadd  12948  grpsubid1  12955  grpsubadd0sub  12957  grpsubadd  12958  grpsubsub  12959  grpaddsubass  12960  grppncan  12961  grpnnncan2  12967  grpsubpropd2  12975  mhmlem  12978  mhmid  12979  mhmmnd  12980  ghmgrp  12982  mulgnnp1  12991  mulgaddcomlem  13006  mulgaddcom  13007  mulginvinv  13009  mulgnn0dir  13013  mulgdirlem  13014  mulgp1  13016  mulgneg2  13017  mulgnn0ass  13019  mulgass  13020  mulgmodid  13022  mulgsubdir  13023  nmzsubg  13070  0nsg  13074  eqger  13083  ablsub4  13116  abladdsub4  13117  ablsubsub4  13122  ablsub32  13125  ablnnncan  13126  mgpress  13141  srgass  13154  srgpcomp  13173  srgpcompp  13174  srgpcomppsc  13175  srg1expzeq1  13178  ringpropd  13217  ringrz  13223  ringnegr  13229  ringmneg2  13231  ringsubdi  13233  ringsubdir  13234  ring1  13236  opprring  13249  mulgass3  13254  dvdsrd  13263  unitgrp  13285  invrfvald  13291  dvr1  13307  dvrass  13308  dvrcan1  13309  dvrcan3  13310  rdivmuldivd  13313  subrginv  13358  subrgdv  13359  islmod  13381  lmodlema  13382  islmodd  13383  lmodvs0  13412  lmodvneg1  13420  lmodvsubval2  13432  lmodsubvs  13433  lmodsubdi  13434  lmodsubdir  13435  lmodprop2d  13438  rmodislmodlem  13440  rmodislmod  13441  cnfldsub  13472  restabs  13678  cnprcl2k  13709  cnrest2r  13740  ispsmet  13826  psmettri2  13831  psmetsym  13832  ismet  13847  isxmet  13848  xmettri2  13864  xmetsym  13871  xmettri3  13877  mettri3  13878  xblss2ps  13907  xblss2  13908  comet  14002  xmetxp  14010  xmetxpbl  14011  txmetcnp  14021  fsumcncntop  14059  cncfi  14068  limccl  14131  ellimc3apf  14132  limccnpcntop  14147  limccnp2lem  14148  reldvg  14151  dvfvalap  14153  eldvap  14154  dvcj  14176  dvfre  14177  dvexp  14178  dvexp2  14179  dvrecap  14180  dvmptaddx  14184  dvmptmulx  14185  dvmptnegcn  14187  dvmptsubcn  14188  dvmptcjx  14189  dveflem  14190  dvef  14191  sin0pilem1  14205  sin0pilem2  14206  efper  14231  sinperlem  14232  efimpi  14243  ptolemy  14248  tangtx  14262  abssinper  14270  cosq34lt1  14274  rpcxpef  14318  rpcxpp1  14330  rpcxpneg  14331  rpcxpsub  14332  rpmulcxp  14333  rpdivcxp  14335  cxpmul  14336  rpcxproot  14337  cxpcom  14360  rpabscxpbnd  14362  rplogbval  14366  rplogbreexp  14374  rplogbzexp  14375  rprelogbmulexp  14377  rprelogbdiv  14378  relogbexpap  14379  rplogbcxp  14384  rpcxplogb  14385  logbgcd1irr  14388  logbgcd1irraplemap  14390  binom4  14400  lgslem1  14404  lgsval  14408  lgsfvalg  14409  lgsval2lem  14414  lgsval4  14424  lgsneg  14428  lgsneg1  14429  lgsmod  14430  lgsdir2  14437  lgsdirprm  14438  lgsdilem2  14440  lgsdi  14441  lgsne0  14442  lgssq2  14445  lgsdirnn0  14451  lgsdinn0  14452  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2sqlem2  14465  2sqlem3  14467  2sqlem4  14468  2sqlem8  14473  2sqlem9  14474  2sqlem10  14475  qdencn  14778  trilpolemclim  14787  trilpolemcl  14788  trilpolemisumle  14789  trilpolemeq1  14791  trilpolemlt1  14792  trilpo  14794  apdifflemf  14797  apdiff  14799  iswomni0  14802  redcwlpolemeq1  14805  redcwlpo  14806  nconstwlpolem0  14813  nconstwlpolemgt0  14814  nconstwlpo  14816  neapmkv  14818