Theorem oveq2d 5722

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 5714	. 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 1299  (class class class)co 5706

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-rex 2381  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-uni 3684  df-br 3876  df-iota 5024  df-fv 5067  df-ov 5709

This theorem is referenced by:  csbov1g  5743  caovassg  5861  caovdig  5877  caovdirg  5880  caov32d  5883  caov4d  5887  caov42d  5889  grprinvlem  5897  grprinvd  5898  grpridd  5899  nnaass  6311  nndi  6312  nnmass  6313  nnmsucr  6314  ecovass  6468  ecoviass  6469  ecovdi  6470  ecovidi  6471  addasspig  7039  mulasspig  7041  distrpig  7042  dfplpq2  7063  mulpipq2  7080  addassnqg  7091  prarloclemarch  7127  prarloclemarch2  7128  ltrnqg  7129  enq0sym  7141  addnq0mo  7156  mulnq0mo  7157  addnnnq0  7158  nq0a0  7166  distrnq0  7168  addassnq0  7171  prarloclemlo  7203  prarloclem3  7206  prarloclem5  7209  prarloclemcalc  7211  addnqprl  7238  addnqpru  7239  prmuloclemcalc  7274  mulnqprl  7277  mulnqpru  7278  distrlem4prl  7293  distrlem4pru  7294  1idprl  7299  1idpru  7300  ltexprlemloc  7316  addcanprleml  7323  addcanprlemu  7324  recexprlem1ssu  7343  ltmprr  7351  caucvgprlemcanl  7353  cauappcvgprlemladdru  7365  cauappcvgprlemladdrl  7366  cauappcvgprlem1  7368  cauappcvgprlemlim  7370  caucvgprlemnkj  7375  caucvgprlemnbj  7376  caucvgprlemdisj  7383  caucvgprlemloc  7384  caucvgprlemcl  7385  caucvgprlemladdrl  7387  caucvgprlem1  7388  caucvgpr  7391  caucvgprprlemell  7394  caucvgprprlemcbv  7396  caucvgprprlemval  7397  caucvgprprlemnkeqj  7399  caucvgprprlemopl  7406  caucvgprprlemlol  7407  caucvgprprlemloc  7412  caucvgprprlemclphr  7414  caucvgprprlemexb  7416  caucvgprprlemaddq  7417  caucvgprprlem1  7418  addcmpblnr  7435  mulcmpblnrlemg  7436  addsrmo  7439  mulsrmo  7440  addsrpr  7441  mulsrpr  7442  ltsrprg  7443  recexgt0sr  7469  mulgt0sr  7473  caucvgsrlemgt1  7490  caucvgsrlemoffval  7491  caucvgsr  7497  mulcnsr  7522  pitoregt0  7536  recidpirqlemcalc  7544  axmulcom  7556  axmulass  7558  axdistr  7559  ax0id  7563  axcnre  7566  recriota  7575  axcaucvglemcau  7583  axcaucvglemres  7584  mulid1  7635  adddirp1d  7664  mul32  7763  mul31  7764  add32  7792  add4  7794  add42  7795  cnegex  7811  addcan2  7814  addsubass  7843  subsub2  7861  nppcan2  7864  sub32  7867  nnncan  7868  sub4  7878  muladd  8013  subdi  8014  mul2neg  8027  submul2  8028  mulsub  8030  mulsubfacd  8047  add20  8103  recexre  8206  rereim  8214  apreap  8215  ltmul1  8220  cru  8230  apreim  8231  mulreim  8232  apadd1  8236  apneg  8239  mulap0  8276  divrecap  8309  divassap  8311  divmulasscomap  8317  divsubdirap  8329  divdivdivap  8334  divmul24ap  8337  divmuleqap  8338  divcanap6  8340  divdivap1  8344  divdivap2  8345  divsubdivap  8349  conjmulap  8350  div2negap  8356  apmul1  8409  cju  8577  nnmulcl  8599  add1p1  8821  sub1m1  8822  cnm2m1cnm3  8823  xp1d2m1eqxm1d2  8824  div4p1lem1div2  8825  un0addcl  8862  un0mulcl  8863  zaddcllemneg  8945  qapne  9281  cnref1o  9290  rexsub  9477  xnegid  9483  xaddcom  9485  xnegdi  9492  xaddass  9493  xaddass2  9494  xpncan  9495  xnpcan  9496  xleadd1a  9497  xsubge0  9505  xposdif  9506  xlesubadd  9507  xadd4d  9509  lincmb01cmp  9627  iccf1o  9628  ige3m2fz  9670  fztp  9699  fzsuc2  9700  fseq1m1p1  9716  fzm1  9721  ige2m1fz1  9730  nn0split  9754  nnsplit  9755  fzval3  9822  zpnn0elfzo1  9826  fzosplitsnm1  9827  fzosplitprm1  9852  fzoshftral  9856  rebtwn2zlemstep  9871  flhalf  9916  modqval  9938  modqvalr  9939  modqdiffl  9949  modqfrac  9951  flqmod  9952  intqfrac  9953  zmod10  9954  modqmulnn  9956  modqvalp1  9957  modqid  9963  modqcyc  9973  modqcyc2  9974  modqmul1  9991  q2submod  9999  modqdi  10006  modqsubdir  10007  modqeqmodmin  10008  modsumfzodifsn  10010  addmodlteq  10012  frecuzrdgsuctlem  10037  uzsinds  10056  seqeq3  10064  iseqvalcbv  10071  seq3val  10072  seqvalcd  10073  seqf  10075  seq3p1  10076  seqovcd  10077  seqp1cd  10080  seq3m1  10082  seq3fveq2  10083  seq3shft2  10087  monoord2  10091  ser3mono  10092  seq3split  10093  seq3caopr3  10095  seq3caopr2  10096  seq3caopr  10097  seq3id2  10123  seq3homo  10124  seq3z  10125  exp3vallem  10135  exp3val  10136  expp1  10141  expnegap0  10142  expineg2  10143  expn1ap0  10144  expm1t  10162  1exp  10163  expnegzap  10168  mulexpzap  10174  expadd  10176  expaddzaplem  10177  expaddzap  10178  expmul  10179  expmulzap  10180  m1expeven  10181  expsubap  10182  expp1zap  10183  expm1ap  10184  expdivap  10185  iexpcyc  10238  subsq2  10241  binom2  10244  binom21  10245  binom2sub  10246  binom2sub1  10247  mulbinom2  10249  binom3  10250  zesq  10251  bernneq  10253  sqoddm1div8  10285  nn0opthlem1d  10307  nn0opthd  10309  facp1  10317  facnn2  10321  faclbnd  10328  faclbnd6  10331  bcval  10336  bccmpl  10341  bcn0  10342  bcnn  10344  bcnp1n  10346  bcm1k  10347  bcp1n  10348  bcp1nk  10349  bcval5  10350  bcp1m1  10352  bcpasc  10353  bcn2m1  10356  bcn2p1  10357  omgadd  10389  hashunlem  10391  hashunsng  10394  hashdifsn  10406  hashxp  10413  zfz1isolemsplit  10422  zfz1isolem1  10424  zfz1iso  10425  seq3coll  10426  shftcan1  10447  shftcan2  10448  cjval  10458  cjth  10459  crre  10470  replim  10472  remim  10473  reim0b  10475  rereb  10476  mulreap  10477  cjreb  10479  recj  10480  reneg  10481  readd  10482  resub  10483  remullem  10484  imcj  10488  imneg  10489  imadd  10490  imsub  10491  cjcj  10496  cjadd  10497  ipcnval  10499  cjmulrcl  10500  cjneg  10503  addcj  10504  cjsub  10505  cnrecnv  10523  caucvgrelemcau  10592  cvg1nlemcau  10596  cvg1nlemres  10597  recvguniqlem  10606  resqrexlemover  10622  resqrexlemlo  10625  resqrexlemcalc1  10626  resqrexlemcalc3  10628  resqrexlemnm  10630  resqrexlemcvg  10631  absneg  10662  abscj  10664  sqabsadd  10667  sqabssub  10668  absmul  10681  absid  10683  absre  10689  absresq  10690  absexpzap  10692  recvalap  10709  abstri  10716  abs2dif2  10719  recan  10721  cau3lem  10726  amgm2  10730  bdtrilem  10849  xrmaxadd  10869  xrbdtri  10884  climaddc1  10937  climsubc1  10940  climcvg1nlem  10957  serf0  10960  summodclem3  10988  summodclem2a  10989  summodc  10991  fsumsplitsn  11018  fsumm1  11024  fsumsplitsnun  11027  fsump1  11028  isummulc2  11034  fsumrev  11051  fisum0diag2  11055  fsummulc2  11056  fsumsub  11060  fsumabs  11073  telfsumo  11074  fsumparts  11078  fsumrelem  11079  fsumiun  11085  binomlem  11091  binom  11092  binom1p  11093  binom11  11094  binom1dif  11095  bcxmas  11097  isumsplit  11099  isum1p  11100  divcnv  11105  arisum2  11107  trireciplem  11108  trirecip  11109  geolim  11119  georeclim  11121  geo2sum  11122  geo2lim  11124  geoisum1c  11128  0.999...  11129  cvgratnnlemnexp  11132  cvgratnnlemmn  11133  cvgratz  11140  mertenslem2  11144  mertensabs  11145  ege2le3  11175  efaddlem  11178  efsub  11185  efexp  11186  eftlub  11194  efsep  11195  effsumlt  11196  ef4p  11198  tanval3ap  11219  resinval  11220  recosval  11221  efi4p  11222  efival  11237  efmival  11238  efeul  11239  sinadd  11241  cosadd  11242  tanaddap  11244  sinsub  11245  cossub  11246  sincossq  11253  sin2t  11254  cos2t  11255  cos2tsin  11256  ef01bndlem  11261  sin01bnd  11262  cos01bnd  11263  absef  11273  absefib  11274  efieq1re  11275  demoivreALT  11277  eirraplem  11278  dvdsexp  11354  oexpneg  11369  opeo  11389  omeo  11390  m1exp1  11393  flodddiv4  11426  flodddiv4t2lthalf  11429  divgcdnnr  11459  gcdaddm  11467  gcdadd  11468  gcdid  11469  modgcd  11474  bezoutlemnewy  11477  bezoutlema  11480  bezoutlemb  11481  bezoutlemex  11482  bezoutlembz  11485  absmulgcd  11498  gcdmultiple  11501  gcdmultiplez  11502  rpmulgcd  11507  rplpwr  11508  eucalginv  11530  eucalg  11533  lcmneg  11548  lcmgcdlem  11551  lcmgcd  11552  lcmid  11554  lcm1  11555  mulgcddvds  11568  qredeq  11570  divgcdcoprmex  11576  prmind2  11594  rpexp1i  11625  pw2dvdslemn  11635  pw2dvdseulemle  11637  pw2dvdseu  11638  oddpwdclemxy  11639  oddpwdclemdvds  11640  oddpwdclemndvds  11641  oddpwdclemdc  11643  2sqpwodd  11646  nn0gcdsq  11670  phiprmpw  11690  hashgcdlem  11695  restabs  12126  cnprcl2k  12156  cnrest2r  12187  ispsmet  12251  psmettri2  12256  psmetsym  12257  ismet  12272  isxmet  12273  xmettri2  12289  xmetsym  12296  xmettri3  12302  mettri3  12303  xblss2ps  12332  xblss2  12333  comet  12427  cncfi  12478  limccl  12510  ellimc3ap  12511  limccnpcntop  12520  reldvg  12521  dvfvalap  12523  eldvap  12524  qdencn  12806  trilpolemclim  12813  trilpolemcl  12814  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818  trilpo  12820