Theorem oveq2d 5890

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 5882	. 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 5874

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 2739  df-un 3133  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877

This theorem is referenced by:  csbov1g  5914  caovassg  6032  caovdig  6048  caovdirg  6051  caov32d  6054  caov4d  6058  caov42d  6060  nnaass  6485  nndi  6486  nnmass  6487  nnmsucr  6488  ecovass  6643  ecoviass  6644  ecovdi  6645  ecovidi  6646  addasspig  7328  mulasspig  7330  distrpig  7331  dfplpq2  7352  mulpipq2  7369  addassnqg  7380  prarloclemarch  7416  prarloclemarch2  7417  ltrnqg  7418  enq0sym  7430  addnq0mo  7445  mulnq0mo  7446  addnnnq0  7447  nq0a0  7455  distrnq0  7457  addassnq0  7460  prarloclemlo  7492  prarloclem3  7495  prarloclem5  7498  prarloclemcalc  7500  addnqprl  7527  addnqpru  7528  prmuloclemcalc  7563  mulnqprl  7566  mulnqpru  7567  distrlem4prl  7582  distrlem4pru  7583  1idprl  7588  1idpru  7589  ltexprlemloc  7605  addcanprleml  7612  addcanprlemu  7613  recexprlem1ssu  7632  ltmprr  7640  caucvgprlemcanl  7642  cauappcvgprlemladdru  7654  cauappcvgprlemladdrl  7655  cauappcvgprlem1  7657  cauappcvgprlemlim  7659  caucvgprlemnkj  7664  caucvgprlemnbj  7665  caucvgprlemdisj  7672  caucvgprlemloc  7673  caucvgprlemcl  7674  caucvgprlemladdrl  7676  caucvgprlem1  7677  caucvgpr  7680  caucvgprprlemell  7683  caucvgprprlemcbv  7685  caucvgprprlemval  7686  caucvgprprlemnkeqj  7688  caucvgprprlemopl  7695  caucvgprprlemlol  7696  caucvgprprlemloc  7701  caucvgprprlemclphr  7703  caucvgprprlemexb  7705  caucvgprprlemaddq  7706  caucvgprprlem1  7707  addcmpblnr  7737  mulcmpblnrlemg  7738  addsrmo  7741  mulsrmo  7742  addsrpr  7743  mulsrpr  7744  ltsrprg  7745  recexgt0sr  7771  mulgt0sr  7776  caucvgsrlemgt1  7793  caucvgsrlemoffval  7794  caucvgsr  7800  suplocsrlemb  7804  suplocsrlempr  7805  suplocsrlem  7806  suplocsr  7807  mulcnsr  7833  pitoregt0  7847  recidpirqlemcalc  7855  axmulcom  7869  axmulass  7871  axdistr  7872  ax0id  7876  axcnre  7879  recriota  7888  axcaucvglemcau  7896  axcaucvglemres  7897  mulrid  7953  adddirp1d  7983  mul32  8086  mul31  8087  add32  8115  add4  8117  add42  8118  cnegex  8134  addcan2  8137  addsubass  8166  subsub2  8184  nppcan2  8187  sub32  8190  nnncan  8191  sub4  8201  muladd  8340  subdi  8341  mul2neg  8354  submul2  8355  mulsub  8357  mulsubfacd  8374  add20  8430  recexre  8534  rereim  8542  apreap  8543  ltmul1  8548  cru  8558  apreim  8559  mulreim  8560  apadd1  8564  apneg  8567  mulap0  8610  divrecap  8644  divassap  8646  divmulasscomap  8652  divsubdirap  8664  divdivdivap  8669  divmul24ap  8672  divmuleqap  8673  divcanap6  8675  divdivap1  8679  divdivap2  8680  divsubdivap  8684  conjmulap  8685  div2negap  8691  apmul1  8744  cju  8917  nnmulcl  8939  add1p1  9167  sub1m1  9168  cnm2m1cnm3  9169  xp1d2m1eqxm1d2  9170  div4p1lem1div2  9171  un0addcl  9208  un0mulcl  9209  zaddcllemneg  9291  qapne  9638  cnref1o  9649  rexsub  9852  xnegid  9858  xaddcom  9860  xnegdi  9867  xaddass  9868  xaddass2  9869  xpncan  9870  xnpcan  9871  xleadd1a  9872  xsubge0  9880  xposdif  9881  xlesubadd  9882  xadd4d  9884  lincmb01cmp  10002  iccf1o  10003  ige3m2fz  10048  fztp  10077  fzsuc2  10078  fseq1m1p1  10094  fzm1  10099  ige2m1fz1  10108  nn0split  10135  nnsplit  10136  fzval3  10203  zpnn0elfzo1  10207  fzosplitsnm1  10208  fzosplitprm1  10233  fzoshftral  10237  rebtwn2zlemstep  10252  flhalf  10301  modqval  10323  modqvalr  10324  modqdiffl  10334  modqfrac  10336  flqmod  10337  intqfrac  10338  zmod10  10339  modqmulnn  10341  modqvalp1  10342  modqid  10348  modqcyc  10358  modqcyc2  10359  modqmul1  10376  q2submod  10384  modqdi  10391  modqsubdir  10392  modqeqmodmin  10393  modsumfzodifsn  10395  addmodlteq  10397  frecuzrdgsuctlem  10422  uzsinds  10441  seqeq3  10449  iseqvalcbv  10456  seq3val  10457  seqvalcd  10458  seqf  10460  seq3p1  10461  seqovcd  10462  seqp1cd  10465  seq3m1  10467  seq3fveq2  10468  seq3shft2  10472  monoord2  10476  ser3mono  10477  seq3split  10478  seq3caopr3  10480  seq3caopr2  10481  seq3caopr  10482  seq3id2  10508  seq3homo  10509  seq3z  10510  exp3vallem  10520  exp3val  10521  expp1  10526  expnegap0  10527  expineg2  10528  expn1ap0  10529  expm1t  10547  1exp  10548  expnegzap  10553  mulexpzap  10559  expadd  10561  expaddzaplem  10562  expaddzap  10563  expmul  10564  expmulzap  10565  m1expeven  10566  expsubap  10567  expp1zap  10568  expm1ap  10569  expdivap  10570  iexpcyc  10624  subsq2  10627  binom2  10631  binom21  10632  binom2sub  10633  binom2sub1  10634  mulbinom2  10636  binom3  10637  zesq  10638  bernneq  10640  sqoddm1div8  10673  mulsubdivbinom2ap  10690  nn0opthlem1d  10699  nn0opthd  10701  facp1  10709  facnn2  10713  faclbnd  10720  faclbnd6  10723  bcval  10728  bccmpl  10733  bcn0  10734  bcnn  10736  bcnp1n  10738  bcm1k  10739  bcp1n  10740  bcp1nk  10741  bcval5  10742  bcp1m1  10744  bcpasc  10745  bcn2m1  10748  bcn2p1  10749  omgadd  10781  hashunlem  10783  hashunsng  10786  hashdifsn  10798  hashxp  10805  zfz1isolemsplit  10817  zfz1isolem1  10819  zfz1iso  10820  seq3coll  10821  shftcan1  10842  shftcan2  10843  cjval  10853  cjth  10854  crre  10865  replim  10867  remim  10868  reim0b  10870  rereb  10871  mulreap  10872  cjreb  10874  recj  10875  reneg  10876  readd  10877  resub  10878  remullem  10879  imcj  10883  imneg  10884  imadd  10885  imsub  10886  cjcj  10891  cjadd  10892  ipcnval  10894  cjmulrcl  10895  cjneg  10898  addcj  10899  cjsub  10900  cnrecnv  10918  caucvgrelemcau  10988  cvg1nlemcau  10992  cvg1nlemres  10993  recvguniqlem  11002  resqrexlemover  11018  resqrexlemlo  11021  resqrexlemcalc1  11022  resqrexlemcalc3  11024  resqrexlemnm  11026  resqrexlemcvg  11027  absneg  11058  abscj  11060  sqabsadd  11063  sqabssub  11064  absmul  11077  absid  11079  absre  11085  absresq  11086  absexpzap  11088  recvalap  11105  abstri  11112  abs2dif2  11115  recan  11117  cau3lem  11122  amgm2  11126  bdtrilem  11246  xrmaxadd  11268  xrbdtri  11283  climaddc1  11336  climsubc1  11339  climcvg1nlem  11356  serf0  11359  summodclem3  11387  summodclem2a  11388  summodc  11390  fsumsplitsn  11417  fsumm1  11423  fsumsplitsnun  11426  fsump1  11427  isummulc2  11433  fsumrev  11450  fisum0diag2  11454  fsummulc2  11455  fsumsub  11459  fsumabs  11472  telfsumo  11473  fsumparts  11477  fsumrelem  11478  fsumiun  11484  binomlem  11490  binom  11491  binom1p  11492  binom11  11493  binom1dif  11494  bcxmas  11496  isumsplit  11498  isum1p  11499  divcnv  11504  arisum2  11506  trireciplem  11507  trirecip  11508  geolim  11518  georeclim  11520  geo2sum  11521  geo2lim  11523  geoisum1c  11527  0.999...  11528  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  cvgratz  11539  mertenslem2  11543  mertensabs  11544  clim2prod  11546  prodfrecap  11553  prodfdivap  11554  prodmodclem3  11582  prodmodclem2a  11583  fprodm1  11605  fprodp1  11607  fprodunsn  11611  fprodfac  11622  fprodeq0  11624  fprodconst  11627  fprodrec  11636  fproddivap  11637  fprodsplitsn  11640  ege2le3  11678  efaddlem  11681  efsub  11688  efexp  11689  eftlub  11697  efsep  11698  effsumlt  11699  ef4p  11701  tanval3ap  11721  resinval  11722  recosval  11723  efi4p  11724  efival  11739  efmival  11740  efeul  11741  sinadd  11743  cosadd  11744  tanaddap  11746  sinsub  11747  cossub  11748  sincossq  11755  sin2t  11756  cos2t  11757  cos2tsin  11758  ef01bndlem  11763  sin01bnd  11764  cos01bnd  11765  cos12dec  11774  absef  11776  absefib  11777  efieq1re  11778  demoivreALT  11780  eirraplem  11783  dvdsexp  11866  oexpneg  11881  opeo  11901  omeo  11902  m1exp1  11905  flodddiv4  11938  flodddiv4t2lthalf  11941  divgcdnnr  11976  gcdaddm  11984  gcdadd  11985  gcdid  11986  modgcd  11991  gcdmultipled  11993  dvdsgcdidd  11994  bezoutlemnewy  11996  bezoutlema  11999  bezoutlemb  12000  bezoutlemex  12001  bezoutlembz  12004  absmulgcd  12017  gcdmultiple  12020  gcdmultiplez  12021  rpmulgcd  12026  rplpwr  12027  eucalginv  12055  eucalg  12058  lcmneg  12073  lcmgcdlem  12076  lcmgcd  12077  lcmid  12079  lcm1  12080  mulgcddvds  12093  qredeq  12095  divgcdcoprmex  12101  prmind2  12119  rpexp1i  12153  pw2dvdslemn  12164  pw2dvdseulemle  12166  pw2dvdseu  12167  oddpwdclemxy  12168  oddpwdclemdvds  12169  oddpwdclemndvds  12170  oddpwdclemdc  12172  2sqpwodd  12175  nn0gcdsq  12199  phiprmpw  12221  eulerthlemrprm  12228  eulerthlema  12229  eulerthlemh  12230  eulerthlemth  12231  fermltl  12233  prmdiv  12234  hashgcdlem  12237  odzdvds  12244  vfermltl  12250  modprm0  12253  nnnn0modprm0  12254  modprmn0modprm0  12255  coprimeprodsq  12256  pythagtriplem1  12264  pythagtriplem4  12267  pythagtriplem12  12274  pythagtriplem14  12276  pythagtriplem16  12278  pythagtriplem18  12280  pythagtrip  12282  pcpremul  12292  pceu  12294  pczpre  12296  pcdiv  12301  pcqmul  12302  pcqdiv  12306  pcexp  12308  pczdvds  12312  pczndvds  12314  pczndvds2  12316  pcid  12322  pcneg  12323  pcdvdstr  12325  pcgcd1  12326  pcgcd  12327  pc2dvds  12328  pcaddlem  12337  pcadd  12338  pcmpt  12340  pcmpt2  12341  fldivp1  12345  pcfac  12347  pcbc  12348  expnprm  12350  prmpwdvds  12352  pockthlem  12353  pockthi  12355  4sqlem7  12381  4sqlem9  12383  4sqlem10  12384  4sqlem2  12386  4sqlem3  12387  4sqlem4  12389  mul4sqlem  12390  setscomd  12502  ressvalsets  12523  strressid  12529  ressval3d  12530  ressinbasd  12532  ressressg  12533  ressabsg  12534  grprinvlem  12803  grprinvd  12804  grpridd  12805  isnsgrp  12811  sgrpass  12813  sgrp1  12815  mnd32g  12827  mnd4g  12829  mndpropd  12840  mhmlin  12857  grprcan  12909  grpsubval  12918  grpinvid2  12924  grpasscan2  12933  grpsubinv  12942  grpinvadd  12947  grpsubid1  12954  grpsubadd0sub  12956  grpsubadd  12957  grpsubsub  12958  grpaddsubass  12959  grppncan  12960  grpnnncan2  12966  grpsubpropd2  12974  mhmlem  12977  mhmid  12978  mhmmnd  12979  ghmgrp  12981  mulgnnp1  12990  mulgaddcomlem  13004  mulgaddcom  13005  mulginvinv  13007  mulgnn0dir  13011  mulgdirlem  13012  mulgp1  13014  mulgneg2  13015  mulgnn0ass  13017  mulgass  13018  mulgmodid  13020  mulgsubdir  13021  nmzsubg  13068  0nsg  13072  eqger  13081  ablsub4  13114  abladdsub4  13115  ablsubsub4  13120  ablsub32  13123  ablnnncan  13124  mgpress  13139  srgass  13152  srgpcomp  13171  srgpcompp  13172  srgpcomppsc  13173  srg1expzeq1  13176  ringpropd  13215  ringrz  13221  rngnegr  13227  ringmneg2  13229  ringsubdi  13231  rngsubdir  13232  ring1  13234  opprring  13247  mulgass3  13252  dvdsrd  13261  unitgrp  13283  invrfvald  13289  dvr1  13305  dvrass  13306  dvrcan1  13307  dvrcan3  13308  rdivmuldivd  13311  subrginv  13356  subrgdv  13357  islmod  13379  lmodlema  13380  islmodd  13381  cnfldsub  13439  restabs  13645  cnprcl2k  13676  cnrest2r  13707  ispsmet  13793  psmettri2  13798  psmetsym  13799  ismet  13814  isxmet  13815  xmettri2  13831  xmetsym  13838  xmettri3  13844  mettri3  13845  xblss2ps  13874  xblss2  13875  comet  13969  xmetxp  13977  xmetxpbl  13978  txmetcnp  13988  fsumcncntop  14026  cncfi  14035  limccl  14098  ellimc3apf  14099  limccnpcntop  14114  limccnp2lem  14115  reldvg  14118  dvfvalap  14120  eldvap  14121  dvcj  14143  dvfre  14144  dvexp  14145  dvexp2  14146  dvrecap  14147  dvmptaddx  14151  dvmptmulx  14152  dvmptnegcn  14154  dvmptsubcn  14155  dvmptcjx  14156  dveflem  14157  dvef  14158  sin0pilem1  14172  sin0pilem2  14173  efper  14198  sinperlem  14199  efimpi  14210  ptolemy  14215  tangtx  14229  abssinper  14237  cosq34lt1  14241  rpcxpef  14285  rpcxpp1  14297  rpcxpneg  14298  rpcxpsub  14299  rpmulcxp  14300  rpdivcxp  14302  cxpmul  14303  rpcxproot  14304  cxpcom  14327  rpabscxpbnd  14329  rplogbval  14333  rplogbreexp  14341  rplogbzexp  14342  rprelogbmulexp  14344  rprelogbdiv  14345  relogbexpap  14346  rplogbcxp  14351  rpcxplogb  14352  logbgcd1irr  14355  logbgcd1irraplemap  14357  binom4  14367  lgslem1  14371  lgsval  14375  lgsfvalg  14376  lgsval2lem  14381  lgsval4  14391  lgsneg  14395  lgsneg1  14396  lgsmod  14397  lgsdir2  14404  lgsdirprm  14405  lgsdilem2  14407  lgsdi  14408  lgsne0  14409  lgssq2  14412  lgsdirnn0  14418  lgsdinn0  14419  lgseisenlem1  14420  lgseisenlem2  14421  m1lgs  14422  2sqlem2  14432  2sqlem3  14434  2sqlem4  14435  2sqlem8  14440  2sqlem9  14441  2sqlem10  14442  qdencn  14745  trilpolemclim  14754  trilpolemcl  14755  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  trilpo  14761  apdifflemf  14764  apdiff  14766  iswomni0  14769  redcwlpolemeq1  14772  redcwlpo  14773  nconstwlpolem0  14780  nconstwlpolemgt0  14781  nconstwlpo  14783  neapmkv  14785