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  7982  mul32  8085  mul31  8086  add32  8114  add4  8116  add42  8117  cnegex  8133  addcan2  8136  addsubass  8165  subsub2  8183  nppcan2  8186  sub32  8189  nnncan  8190  sub4  8200  muladd  8339  subdi  8340  mul2neg  8353  submul2  8354  mulsub  8356  mulsubfacd  8373  add20  8429  recexre  8533  rereim  8541  apreap  8542  ltmul1  8547  cru  8557  apreim  8558  mulreim  8559  apadd1  8563  apneg  8566  mulap0  8609  divrecap  8643  divassap  8645  divmulasscomap  8651  divsubdirap  8663  divdivdivap  8668  divmul24ap  8671  divmuleqap  8672  divcanap6  8674  divdivap1  8678  divdivap2  8679  divsubdivap  8683  conjmulap  8684  div2negap  8690  apmul1  8743  cju  8916  nnmulcl  8938  add1p1  9166  sub1m1  9167  cnm2m1cnm3  9168  xp1d2m1eqxm1d2  9169  div4p1lem1div2  9170  un0addcl  9207  un0mulcl  9208  zaddcllemneg  9290  qapne  9637  cnref1o  9648  rexsub  9851  xnegid  9857  xaddcom  9859  xnegdi  9866  xaddass  9867  xaddass2  9868  xpncan  9869  xnpcan  9870  xleadd1a  9871  xsubge0  9879  xposdif  9880  xlesubadd  9881  xadd4d  9883  lincmb01cmp  10001  iccf1o  10002  ige3m2fz  10046  fztp  10075  fzsuc2  10076  fseq1m1p1  10092  fzm1  10097  ige2m1fz1  10106  nn0split  10133  nnsplit  10134  fzval3  10201  zpnn0elfzo1  10205  fzosplitsnm1  10206  fzosplitprm1  10231  fzoshftral  10235  rebtwn2zlemstep  10250  flhalf  10299  modqval  10321  modqvalr  10322  modqdiffl  10332  modqfrac  10334  flqmod  10335  intqfrac  10336  zmod10  10337  modqmulnn  10339  modqvalp1  10340  modqid  10346  modqcyc  10356  modqcyc2  10357  modqmul1  10374  q2submod  10382  modqdi  10389  modqsubdir  10390  modqeqmodmin  10391  modsumfzodifsn  10393  addmodlteq  10395  frecuzrdgsuctlem  10420  uzsinds  10439  seqeq3  10447  iseqvalcbv  10454  seq3val  10455  seqvalcd  10456  seqf  10458  seq3p1  10459  seqovcd  10460  seqp1cd  10463  seq3m1  10465  seq3fveq2  10466  seq3shft2  10470  monoord2  10474  ser3mono  10475  seq3split  10476  seq3caopr3  10478  seq3caopr2  10479  seq3caopr  10480  seq3id2  10506  seq3homo  10507  seq3z  10508  exp3vallem  10518  exp3val  10519  expp1  10524  expnegap0  10525  expineg2  10526  expn1ap0  10527  expm1t  10545  1exp  10546  expnegzap  10551  mulexpzap  10557  expadd  10559  expaddzaplem  10560  expaddzap  10561  expmul  10562  expmulzap  10563  m1expeven  10564  expsubap  10565  expp1zap  10566  expm1ap  10567  expdivap  10568  iexpcyc  10621  subsq2  10624  binom2  10628  binom21  10629  binom2sub  10630  binom2sub1  10631  mulbinom2  10633  binom3  10634  zesq  10635  bernneq  10637  sqoddm1div8  10670  nn0opthlem1d  10695  nn0opthd  10697  facp1  10705  facnn2  10709  faclbnd  10716  faclbnd6  10719  bcval  10724  bccmpl  10729  bcn0  10730  bcnn  10732  bcnp1n  10734  bcm1k  10735  bcp1n  10736  bcp1nk  10737  bcval5  10738  bcp1m1  10740  bcpasc  10741  bcn2m1  10744  bcn2p1  10745  omgadd  10777  hashunlem  10779  hashunsng  10782  hashdifsn  10794  hashxp  10801  zfz1isolemsplit  10813  zfz1isolem1  10815  zfz1iso  10816  seq3coll  10817  shftcan1  10838  shftcan2  10839  cjval  10849  cjth  10850  crre  10861  replim  10863  remim  10864  reim0b  10866  rereb  10867  mulreap  10868  cjreb  10870  recj  10871  reneg  10872  readd  10873  resub  10874  remullem  10875  imcj  10879  imneg  10880  imadd  10881  imsub  10882  cjcj  10887  cjadd  10888  ipcnval  10890  cjmulrcl  10891  cjneg  10894  addcj  10895  cjsub  10896  cnrecnv  10914  caucvgrelemcau  10984  cvg1nlemcau  10988  cvg1nlemres  10989  recvguniqlem  10998  resqrexlemover  11014  resqrexlemlo  11017  resqrexlemcalc1  11018  resqrexlemcalc3  11020  resqrexlemnm  11022  resqrexlemcvg  11023  absneg  11054  abscj  11056  sqabsadd  11059  sqabssub  11060  absmul  11073  absid  11075  absre  11081  absresq  11082  absexpzap  11084  recvalap  11101  abstri  11108  abs2dif2  11111  recan  11113  cau3lem  11118  amgm2  11122  bdtrilem  11242  xrmaxadd  11264  xrbdtri  11279  climaddc1  11332  climsubc1  11335  climcvg1nlem  11352  serf0  11355  summodclem3  11383  summodclem2a  11384  summodc  11386  fsumsplitsn  11413  fsumm1  11419  fsumsplitsnun  11422  fsump1  11423  isummulc2  11429  fsumrev  11446  fisum0diag2  11450  fsummulc2  11451  fsumsub  11455  fsumabs  11468  telfsumo  11469  fsumparts  11473  fsumrelem  11474  fsumiun  11480  binomlem  11486  binom  11487  binom1p  11488  binom11  11489  binom1dif  11490  bcxmas  11492  isumsplit  11494  isum1p  11495  divcnv  11500  arisum2  11502  trireciplem  11503  trirecip  11504  geolim  11514  georeclim  11516  geo2sum  11517  geo2lim  11519  geoisum1c  11523  0.999...  11524  cvgratnnlemnexp  11527  cvgratnnlemmn  11528  cvgratz  11535  mertenslem2  11539  mertensabs  11540  clim2prod  11542  prodfrecap  11549  prodfdivap  11550  prodmodclem3  11578  prodmodclem2a  11579  fprodm1  11601  fprodp1  11603  fprodunsn  11607  fprodfac  11618  fprodeq0  11620  fprodconst  11623  fprodrec  11632  fproddivap  11633  fprodsplitsn  11636  ege2le3  11674  efaddlem  11677  efsub  11684  efexp  11685  eftlub  11693  efsep  11694  effsumlt  11695  ef4p  11697  tanval3ap  11717  resinval  11718  recosval  11719  efi4p  11720  efival  11735  efmival  11736  efeul  11737  sinadd  11739  cosadd  11740  tanaddap  11742  sinsub  11743  cossub  11744  sincossq  11751  sin2t  11752  cos2t  11753  cos2tsin  11754  ef01bndlem  11759  sin01bnd  11760  cos01bnd  11761  cos12dec  11770  absef  11772  absefib  11773  efieq1re  11774  demoivreALT  11776  eirraplem  11779  dvdsexp  11861  oexpneg  11876  opeo  11896  omeo  11897  m1exp1  11900  flodddiv4  11933  flodddiv4t2lthalf  11936  divgcdnnr  11971  gcdaddm  11979  gcdadd  11980  gcdid  11981  modgcd  11986  gcdmultipled  11988  dvdsgcdidd  11989  bezoutlemnewy  11991  bezoutlema  11994  bezoutlemb  11995  bezoutlemex  11996  bezoutlembz  11999  absmulgcd  12012  gcdmultiple  12015  gcdmultiplez  12016  rpmulgcd  12021  rplpwr  12022  eucalginv  12050  eucalg  12053  lcmneg  12068  lcmgcdlem  12071  lcmgcd  12072  lcmid  12074  lcm1  12075  mulgcddvds  12088  qredeq  12090  divgcdcoprmex  12096  prmind2  12114  rpexp1i  12148  pw2dvdslemn  12159  pw2dvdseulemle  12161  pw2dvdseu  12162  oddpwdclemxy  12163  oddpwdclemdvds  12164  oddpwdclemndvds  12165  oddpwdclemdc  12167  2sqpwodd  12170  nn0gcdsq  12194  phiprmpw  12216  eulerthlemrprm  12223  eulerthlema  12224  eulerthlemh  12225  eulerthlemth  12226  fermltl  12228  prmdiv  12229  hashgcdlem  12232  odzdvds  12239  vfermltl  12245  modprm0  12248  nnnn0modprm0  12249  modprmn0modprm0  12250  coprimeprodsq  12251  pythagtriplem1  12259  pythagtriplem4  12262  pythagtriplem12  12269  pythagtriplem14  12271  pythagtriplem16  12273  pythagtriplem18  12275  pythagtrip  12277  pcpremul  12287  pceu  12289  pczpre  12291  pcdiv  12296  pcqmul  12297  pcqdiv  12301  pcexp  12303  pczdvds  12307  pczndvds  12309  pczndvds2  12311  pcid  12317  pcneg  12318  pcdvdstr  12320  pcgcd1  12321  pcgcd  12322  pc2dvds  12323  pcaddlem  12332  pcadd  12333  pcmpt  12335  pcmpt2  12336  fldivp1  12340  pcfac  12342  pcbc  12343  expnprm  12345  prmpwdvds  12347  pockthlem  12348  pockthi  12350  4sqlem7  12376  4sqlem9  12378  4sqlem10  12379  4sqlem2  12381  4sqlem3  12382  4sqlem4  12384  mul4sqlem  12385  setscomd  12497  ressvalsets  12518  strressid  12524  ressval3d  12525  ressinbasd  12527  ressressg  12528  ressabsg  12529  grprinvlem  12758  grprinvd  12759  grpridd  12760  isnsgrp  12766  sgrpass  12768  sgrp1  12770  mnd32g  12782  mnd4g  12784  mndpropd  12795  mhmlin  12812  grprcan  12864  grpsubval  12873  grpinvid2  12879  grpasscan2  12888  grpsubinv  12897  grpinvadd  12902  grpsubid1  12909  grpsubadd0sub  12911  grpsubadd  12912  grpsubsub  12913  grpaddsubass  12914  grppncan  12915  grpnnncan2  12921  grpsubpropd2  12929  mhmlem  12932  mhmid  12933  mhmmnd  12934  ghmgrp  12936  mulgnnp1  12945  mulgaddcomlem  12959  mulgaddcom  12960  mulginvinv  12962  mulgnn0dir  12966  mulgdirlem  12967  mulgp1  12969  mulgneg2  12970  mulgnn0ass  12972  mulgass  12973  mulgmodid  12975  mulgsubdir  12976  nmzsubg  13023  0nsg  13027  eqger  13036  ablsub4  13069  abladdsub4  13070  ablsubsub4  13075  ablsub32  13078  ablnnncan  13079  mgpress  13094  srgass  13107  srgpcomp  13126  srgpcompp  13127  srgpcomppsc  13128  srg1expzeq1  13131  ringpropd  13170  ringrz  13176  rngnegr  13182  ringmneg2  13184  ringsubdi  13186  rngsubdir  13187  ring1  13189  opprring  13202  mulgass3  13207  dvdsrd  13216  unitgrp  13238  invrfvald  13244  dvr1  13260  dvrass  13261  dvrcan1  13262  dvrcan3  13263  rdivmuldivd  13266  subrginv  13318  subrgdv  13319  cnfldsub  13360  restabs  13568  cnprcl2k  13599  cnrest2r  13630  ispsmet  13716  psmettri2  13721  psmetsym  13722  ismet  13737  isxmet  13738  xmettri2  13754  xmetsym  13761  xmettri3  13767  mettri3  13768  xblss2ps  13797  xblss2  13798  comet  13892  xmetxp  13900  xmetxpbl  13901  txmetcnp  13911  fsumcncntop  13949  cncfi  13958  limccl  14021  ellimc3apf  14022  limccnpcntop  14037  limccnp2lem  14038  reldvg  14041  dvfvalap  14043  eldvap  14044  dvcj  14066  dvfre  14067  dvexp  14068  dvexp2  14069  dvrecap  14070  dvmptaddx  14074  dvmptmulx  14075  dvmptnegcn  14077  dvmptsubcn  14078  dvmptcjx  14079  dveflem  14080  dvef  14081  sin0pilem1  14095  sin0pilem2  14096  efper  14121  sinperlem  14122  efimpi  14133  ptolemy  14138  tangtx  14152  abssinper  14160  cosq34lt1  14164  rpcxpef  14208  rpcxpp1  14220  rpcxpneg  14221  rpcxpsub  14222  rpmulcxp  14223  rpdivcxp  14225  cxpmul  14226  rpcxproot  14227  cxpcom  14250  rpabscxpbnd  14252  rplogbval  14256  rplogbreexp  14264  rplogbzexp  14265  rprelogbmulexp  14267  rprelogbdiv  14268  relogbexpap  14269  rplogbcxp  14274  rpcxplogb  14275  logbgcd1irr  14278  logbgcd1irraplemap  14280  binom4  14290  lgslem1  14294  lgsval  14298  lgsfvalg  14299  lgsval2lem  14304  lgsval4  14314  lgsneg  14318  lgsneg1  14319  lgsmod  14320  lgsdir2  14327  lgsdirprm  14328  lgsdilem2  14330  lgsdi  14331  lgsne0  14332  lgssq2  14335  lgsdirnn0  14341  lgsdinn0  14342  2sqlem2  14344  2sqlem3  14346  2sqlem4  14347  2sqlem8  14352  2sqlem9  14353  2sqlem10  14354  qdencn  14657  trilpolemclim  14666  trilpolemcl  14667  trilpolemisumle  14668  trilpolemeq1  14670  trilpolemlt1  14671  trilpo  14673  apdifflemf  14676  apdiff  14678  iswomni0  14681  redcwlpolemeq1  14684  redcwlpo  14685  nconstwlpolem0  14692  nconstwlpolemgt0  14693  nconstwlpo  14695  neapmkv  14697