Theorem oveq2d 5790

Description: Equality deduction for operation value. (Contributed by NM, 13-Mar-1995.)

Hypothesis

Ref	Expression
oveq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
oveq2d	⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Proof of Theorem oveq2d

Step	Hyp	Ref	Expression
1		oveq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		oveq2 5782	. 2 ⊢ (𝐴 = 𝐵 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐶𝐹𝐴) = (𝐶𝐹𝐵))

Syntax hints:   → wi 4   = wceq 1331  (class class class)co 5774

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-rex 2422  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-br 3930  df-iota 5088  df-fv 5131  df-ov 5777

This theorem is referenced by:  csbov1g  5811  caovassg  5929  caovdig  5945  caovdirg  5948  caov32d  5951  caov4d  5955  caov42d  5957  grprinvlem  5965  grprinvd  5966  grpridd  5967  nnaass  6381  nndi  6382  nnmass  6383  nnmsucr  6384  ecovass  6538  ecoviass  6539  ecovdi  6540  ecovidi  6541  addasspig  7138  mulasspig  7140  distrpig  7141  dfplpq2  7162  mulpipq2  7179  addassnqg  7190  prarloclemarch  7226  prarloclemarch2  7227  ltrnqg  7228  enq0sym  7240  addnq0mo  7255  mulnq0mo  7256  addnnnq0  7257  nq0a0  7265  distrnq0  7267  addassnq0  7270  prarloclemlo  7302  prarloclem3  7305  prarloclem5  7308  prarloclemcalc  7310  addnqprl  7337  addnqpru  7338  prmuloclemcalc  7373  mulnqprl  7376  mulnqpru  7377  distrlem4prl  7392  distrlem4pru  7393  1idprl  7398  1idpru  7399  ltexprlemloc  7415  addcanprleml  7422  addcanprlemu  7423  recexprlem1ssu  7442  ltmprr  7450  caucvgprlemcanl  7452  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  cauappcvgprlem1  7467  cauappcvgprlemlim  7469  caucvgprlemnkj  7474  caucvgprlemnbj  7475  caucvgprlemdisj  7482  caucvgprlemloc  7483  caucvgprlemcl  7484  caucvgprlemladdrl  7486  caucvgprlem1  7487  caucvgpr  7490  caucvgprprlemell  7493  caucvgprprlemcbv  7495  caucvgprprlemval  7496  caucvgprprlemnkeqj  7498  caucvgprprlemopl  7505  caucvgprprlemlol  7506  caucvgprprlemloc  7511  caucvgprprlemclphr  7513  caucvgprprlemexb  7515  caucvgprprlemaddq  7516  caucvgprprlem1  7517  addcmpblnr  7547  mulcmpblnrlemg  7548  addsrmo  7551  mulsrmo  7552  addsrpr  7553  mulsrpr  7554  ltsrprg  7555  recexgt0sr  7581  mulgt0sr  7586  caucvgsrlemgt1  7603  caucvgsrlemoffval  7604  caucvgsr  7610  suplocsrlemb  7614  suplocsrlempr  7615  suplocsrlem  7616  suplocsr  7617  mulcnsr  7643  pitoregt0  7657  recidpirqlemcalc  7665  axmulcom  7679  axmulass  7681  axdistr  7682  ax0id  7686  axcnre  7689  recriota  7698  axcaucvglemcau  7706  axcaucvglemres  7707  mulid1  7763  adddirp1d  7792  mul32  7892  mul31  7893  add32  7921  add4  7923  add42  7924  cnegex  7940  addcan2  7943  addsubass  7972  subsub2  7990  nppcan2  7993  sub32  7996  nnncan  7997  sub4  8007  muladd  8146  subdi  8147  mul2neg  8160  submul2  8161  mulsub  8163  mulsubfacd  8180  add20  8236  recexre  8340  rereim  8348  apreap  8349  ltmul1  8354  cru  8364  apreim  8365  mulreim  8366  apadd1  8370  apneg  8373  mulap0  8415  divrecap  8448  divassap  8450  divmulasscomap  8456  divsubdirap  8468  divdivdivap  8473  divmul24ap  8476  divmuleqap  8477  divcanap6  8479  divdivap1  8483  divdivap2  8484  divsubdivap  8488  conjmulap  8489  div2negap  8495  apmul1  8548  cju  8719  nnmulcl  8741  add1p1  8969  sub1m1  8970  cnm2m1cnm3  8971  xp1d2m1eqxm1d2  8972  div4p1lem1div2  8973  un0addcl  9010  un0mulcl  9011  zaddcllemneg  9093  qapne  9431  cnref1o  9440  rexsub  9636  xnegid  9642  xaddcom  9644  xnegdi  9651  xaddass  9652  xaddass2  9653  xpncan  9654  xnpcan  9655  xleadd1a  9656  xsubge0  9664  xposdif  9665  xlesubadd  9666  xadd4d  9668  lincmb01cmp  9786  iccf1o  9787  ige3m2fz  9829  fztp  9858  fzsuc2  9859  fseq1m1p1  9875  fzm1  9880  ige2m1fz1  9889  nn0split  9913  nnsplit  9914  fzval3  9981  zpnn0elfzo1  9985  fzosplitsnm1  9986  fzosplitprm1  10011  fzoshftral  10015  rebtwn2zlemstep  10030  flhalf  10075  modqval  10097  modqvalr  10098  modqdiffl  10108  modqfrac  10110  flqmod  10111  intqfrac  10112  zmod10  10113  modqmulnn  10115  modqvalp1  10116  modqid  10122  modqcyc  10132  modqcyc2  10133  modqmul1  10150  q2submod  10158  modqdi  10165  modqsubdir  10166  modqeqmodmin  10167  modsumfzodifsn  10169  addmodlteq  10171  frecuzrdgsuctlem  10196  uzsinds  10215  seqeq3  10223  iseqvalcbv  10230  seq3val  10231  seqvalcd  10232  seqf  10234  seq3p1  10235  seqovcd  10236  seqp1cd  10239  seq3m1  10241  seq3fveq2  10242  seq3shft2  10246  monoord2  10250  ser3mono  10251  seq3split  10252  seq3caopr3  10254  seq3caopr2  10255  seq3caopr  10256  seq3id2  10282  seq3homo  10283  seq3z  10284  exp3vallem  10294  exp3val  10295  expp1  10300  expnegap0  10301  expineg2  10302  expn1ap0  10303  expm1t  10321  1exp  10322  expnegzap  10327  mulexpzap  10333  expadd  10335  expaddzaplem  10336  expaddzap  10337  expmul  10338  expmulzap  10339  m1expeven  10340  expsubap  10341  expp1zap  10342  expm1ap  10343  expdivap  10344  iexpcyc  10397  subsq2  10400  binom2  10403  binom21  10404  binom2sub  10405  binom2sub1  10406  mulbinom2  10408  binom3  10409  zesq  10410  bernneq  10412  sqoddm1div8  10444  nn0opthlem1d  10466  nn0opthd  10468  facp1  10476  facnn2  10480  faclbnd  10487  faclbnd6  10490  bcval  10495  bccmpl  10500  bcn0  10501  bcnn  10503  bcnp1n  10505  bcm1k  10506  bcp1n  10507  bcp1nk  10508  bcval5  10509  bcp1m1  10511  bcpasc  10512  bcn2m1  10515  bcn2p1  10516  omgadd  10548  hashunlem  10550  hashunsng  10553  hashdifsn  10565  hashxp  10572  zfz1isolemsplit  10581  zfz1isolem1  10583  zfz1iso  10584  seq3coll  10585  shftcan1  10606  shftcan2  10607  cjval  10617  cjth  10618  crre  10629  replim  10631  remim  10632  reim0b  10634  rereb  10635  mulreap  10636  cjreb  10638  recj  10639  reneg  10640  readd  10641  resub  10642  remullem  10643  imcj  10647  imneg  10648  imadd  10649  imsub  10650  cjcj  10655  cjadd  10656  ipcnval  10658  cjmulrcl  10659  cjneg  10662  addcj  10663  cjsub  10664  cnrecnv  10682  caucvgrelemcau  10752  cvg1nlemcau  10756  cvg1nlemres  10757  recvguniqlem  10766  resqrexlemover  10782  resqrexlemlo  10785  resqrexlemcalc1  10786  resqrexlemcalc3  10788  resqrexlemnm  10790  resqrexlemcvg  10791  absneg  10822  abscj  10824  sqabsadd  10827  sqabssub  10828  absmul  10841  absid  10843  absre  10849  absresq  10850  absexpzap  10852  recvalap  10869  abstri  10876  abs2dif2  10879  recan  10881  cau3lem  10886  amgm2  10890  bdtrilem  11010  xrmaxadd  11030  xrbdtri  11045  climaddc1  11098  climsubc1  11101  climcvg1nlem  11118  serf0  11121  summodclem3  11149  summodclem2a  11150  summodc  11152  fsumsplitsn  11179  fsumm1  11185  fsumsplitsnun  11188  fsump1  11189  isummulc2  11195  fsumrev  11212  fisum0diag2  11216  fsummulc2  11217  fsumsub  11221  fsumabs  11234  telfsumo  11235  fsumparts  11239  fsumrelem  11240  fsumiun  11246  binomlem  11252  binom  11253  binom1p  11254  binom11  11255  binom1dif  11256  bcxmas  11258  isumsplit  11260  isum1p  11261  divcnv  11266  arisum2  11268  trireciplem  11269  trirecip  11270  geolim  11280  georeclim  11282  geo2sum  11283  geo2lim  11285  geoisum1c  11289  0.999...  11290  cvgratnnlemnexp  11293  cvgratnnlemmn  11294  cvgratz  11301  mertenslem2  11305  mertensabs  11306  clim2prod  11308  prodfrecap  11315  prodfdivap  11316  prodmodclem3  11344  prodmodclem2a  11345  ege2le3  11377  efaddlem  11380  efsub  11387  efexp  11388  eftlub  11396  efsep  11397  effsumlt  11398  ef4p  11400  tanval3ap  11421  resinval  11422  recosval  11423  efi4p  11424  efival  11439  efmival  11440  efeul  11441  sinadd  11443  cosadd  11444  tanaddap  11446  sinsub  11447  cossub  11448  sincossq  11455  sin2t  11456  cos2t  11457  cos2tsin  11458  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  cos12dec  11474  absef  11476  absefib  11477  efieq1re  11478  demoivreALT  11480  eirraplem  11483  dvdsexp  11559  oexpneg  11574  opeo  11594  omeo  11595  m1exp1  11598  flodddiv4  11631  flodddiv4t2lthalf  11634  divgcdnnr  11664  gcdaddm  11672  gcdadd  11673  gcdid  11674  modgcd  11679  gcdmultipled  11681  dvdsgcdidd  11682  bezoutlemnewy  11684  bezoutlema  11687  bezoutlemb  11688  bezoutlemex  11689  bezoutlembz  11692  absmulgcd  11705  gcdmultiple  11708  gcdmultiplez  11709  rpmulgcd  11714  rplpwr  11715  eucalginv  11737  eucalg  11740  lcmneg  11755  lcmgcdlem  11758  lcmgcd  11759  lcmid  11761  lcm1  11762  mulgcddvds  11775  qredeq  11777  divgcdcoprmex  11783  prmind2  11801  rpexp1i  11832  pw2dvdslemn  11843  pw2dvdseulemle  11845  pw2dvdseu  11846  oddpwdclemxy  11847  oddpwdclemdvds  11848  oddpwdclemndvds  11849  oddpwdclemdc  11851  2sqpwodd  11854  nn0gcdsq  11878  phiprmpw  11898  hashgcdlem  11903  restabs  12344  cnprcl2k  12375  cnrest2r  12406  ispsmet  12492  psmettri2  12497  psmetsym  12498  ismet  12513  isxmet  12514  xmettri2  12530  xmetsym  12537  xmettri3  12543  mettri3  12544  xblss2ps  12573  xblss2  12574  comet  12668  xmetxp  12676  xmetxpbl  12677  txmetcnp  12687  fsumcncntop  12725  cncfi  12734  limccl  12797  ellimc3apf  12798  limccnpcntop  12813  limccnp2lem  12814  reldvg  12817  dvfvalap  12819  eldvap  12820  dvcj  12842  dvfre  12843  dvexp  12844  dvexp2  12845  dvrecap  12846  dvmptaddx  12850  dvmptmulx  12851  dvmptnegcn  12853  dvmptsubcn  12854  dveflem  12855  dvef  12856  sin0pilem1  12862  sin0pilem2  12863  efper  12888  sinperlem  12889  efimpi  12900  ptolemy  12905  tangtx  12919  abssinper  12927  cosq34lt1  12931  qdencn  13222  trilpolemclim  13229  trilpolemcl  13230  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234  trilpo  13236