Theorem oveq1d 6022

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

Hypothesis

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

Assertion

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

Proof of Theorem oveq1d

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

Syntax hints:   → wi 4   = wceq 1395  (class class class)co 6007

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-iota 5278  df-fv 5326  df-ov 6010

This theorem is referenced by:  fvoveq1d  6029  csbov2g  6049  caovassg  6170  caovdig  6186  caovdirg  6189  caov12d  6193  caov31d  6194  caov411d  6197  caofinvl  6250  omsuc  6626  nnmsucr  6642  nnm1  6679  nnm2  6680  ecovass  6799  ecoviass  6800  ecovdi  6801  ecovidi  6802  isacnm  7396  addasspig  7528  mulasspig  7530  mulpipq2  7569  distrnqg  7585  ltsonq  7596  ltanqg  7598  ltmnqg  7599  ltexnqq  7606  archnqq  7615  prarloclemarch2  7617  enq0sym  7630  addnq0mo  7645  mulnq0mo  7646  addnnnq0  7647  nqpnq0nq  7651  nq0m0r  7654  nq0a0  7655  nnanq0  7656  distrnq0  7657  addassnq0  7660  addpinq1  7662  prarloclemlo  7692  prarloclem3  7695  prarloclem5  7698  prarloclemcalc  7700  addnqprllem  7725  addnqprulem  7726  appdivnq  7761  recexprlem1ssl  7831  recexprlem1ssu  7832  ltmprr  7840  cauappcvgprlemladdru  7854  cauappcvgprlem1  7857  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemcl  7874  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprlem1  7877  caucvgprprlemcbv  7885  caucvgprprlemval  7886  caucvgprprlemexb  7905  caucvgprprlem1  7907  addcmpblnr  7937  mulcmpblnrlemg  7938  addsrmo  7941  mulsrmo  7942  addsrpr  7943  mulsrpr  7944  ltsrprg  7945  1idsr  7966  pn0sr  7969  recexgt0sr  7971  mulgt0sr  7976  srpospr  7981  prsradd  7984  caucvgsrlemfv  7989  caucvgsrlemcau  7991  caucvgsrlemgt1  7993  caucvgsrlemoffval  7994  caucvgsrlemoffcau  7996  caucvgsrlemoffres  7998  caucvgsrlembnd  7999  caucvgsr  8000  map2psrprg  8003  pitonnlem1p1  8044  pitonnlem2  8045  pitonn  8046  recidpirqlemcalc  8055  ax1rid  8075  axrnegex  8077  axcnre  8079  recriota  8088  nntopi  8092  axcaucvglemval  8095  axcaucvglemcau  8096  axcaucvglemres  8097  mul12  8286  mul4  8289  muladd11  8290  readdcan  8297  muladd11r  8313  add12  8315  cnegex  8335  addcan  8337  negeu  8348  pncan2  8364  addsubass  8367  addsub  8368  2addsub  8371  addsubeq4  8372  subid  8376  subid1  8377  npncan  8378  nppcan  8379  nnpcan  8380  nnncan1  8393  npncan3  8395  pnpcan  8396  pnncan  8398  ppncan  8399  addsub4  8400  negsub  8405  subneg  8406  subeqxfrd  8520  mvlraddd  8521  mvlladdd  8522  mvrraddd  8523  subaddeqd  8526  ine0  8551  mulneg1  8552  ltadd2  8577  apreap  8745  cru  8760  recexap  8811  mulcanapd  8819  div23ap  8849  div13ap  8851  divmulassap  8853  divmulasscomap  8854  divcanap4  8857  muldivdirap  8865  divsubdirap  8866  divmuldivap  8870  divdivdivap  8871  divcanap5  8872  divmul13ap  8873  divmuleqap  8875  divdiv32ap  8878  divcanap7  8879  dmdcanap  8880  divdivap1  8881  divdivap2  8882  divadddivap  8885  divsubdivap  8886  conjmulap  8887  divneg2ap  8894  subrecap  8997  mvllmulapd  9000  lt2mul2div  9037  nndivtr  9163  2halves  9351  halfaddsub  9356  subhalfhalf  9357  avgle1  9363  avgle2  9364  div4p1lem1div2  9376  un0addcl  9413  un0mulcl  9414  peano2z  9493  zneo  9559  nneoor  9560  nneo  9561  zeo  9563  zeo2  9564  deceq1  9593  qreccl  9849  xaddcom  10069  xnegdi  10076  xaddass  10077  xaddass2  10078  xpncan  10079  xleadd1a  10081  xltadd1  10084  xposdif  10090  xadd4d  10093  lincmb01cmp  10211  iccf1o  10212  fz0to4untppr  10332  fzo0addel  10406  fzosubel3  10414  qavgle  10490  2tnp1ge0ge0  10533  fldiv4p1lem1div2  10537  fldiv4lem1div2  10539  ceilqm1lt  10546  flqdiv  10555  modqlt  10567  modqdiffl  10569  modqcyc2  10594  modqaddabs  10596  mulqaddmodid  10598  mulp1mod1  10599  modqmuladd  10600  modqmuladdnn0  10602  qnegmod  10603  addmodid  10606  addmodidr  10607  modqadd2mod  10608  modqm1p1mod0  10609  modqmul12d  10612  modqnegd  10613  modqadd12d  10614  modqsub12d  10615  q2submod  10619  modqmulmodr  10624  modqaddmulmod  10625  modqsubdir  10627  modfzo0difsn  10629  modsumfzodifsn  10630  addmodlteq  10632  frecuzrdgsuc  10648  frecfzennn  10660  iseqovex  10692  seq3-1p  10724  seq3caopr2  10727  seqcaopr2g  10728  seq3caopr  10729  seqcaoprg  10730  seqf1oglem2a  10752  seqf1oglem1  10753  seqf1oglem2  10754  seq3id  10759  seq3homo  10761  seq3z  10762  seqhomog  10764  seqfeq4g  10765  expp1  10780  exprecap  10814  expaddzaplem  10816  expmulzap  10819  expdivap  10824  sqval  10831  sqsubswap  10833  sqdividap  10838  subsq  10880  subsq2  10881  binom2  10885  binom2sub  10887  mulbinom2  10890  binom3  10891  zesq  10892  bernneq2  10895  modqexp  10900  sqoddm1div8  10927  mulsubdivbinom2ap  10945  nn0opthlem1d  10954  nn0opthd  10956  nn0opth2d  10957  facp1  10964  facdiv  10972  facndiv  10973  faclbnd  10975  faclbnd2  10976  faclbnd3  10977  bcval  10983  bccmpl  10988  bcm1k  10994  bcp1n  10995  bcp1nk  10996  bcval5  10997  bcp1m1  10999  bcpasc  11000  bcn2m1  11003  hashprg  11043  hashdifpr  11055  hashfzo  11057  hashfzp1  11059  hashfz0  11060  hashxp  11061  zfz1isolemsplit  11073  zfz1isolem1  11075  seq3coll  11077  lswwrd  11131  ccatfvalfi  11140  ccatass  11156  lswccatn0lsw  11159  ccatswrd  11217  ccatpfx  11248  swrdpfx  11254  pfxpfx  11255  ccats1pfxeq  11261  wrdeqs1cat  11267  wrdind  11269  wrd2ind  11270  pfxccatpfx2  11284  pfxccatin12d  11292  cats1catd  11315  cats2catd  11316  s2leng  11336  reval  11375  crre  11383  remim  11386  remul2  11399  immul2  11406  imval2  11420  cjdivap  11435  caucvgre  11507  cvg1nlemcau  11510  cvg1nlemres  11511  resqrexlemp1rp  11532  resqrexlemfp1  11535  resqrexlemover  11536  resqrexlemcalc1  11540  resqrexlemcalc3  11542  resqrexlemnm  11544  resqrexlemoverl  11547  resqrexlemglsq  11548  resqrexlemga  11549  resqrexlemsqa  11550  resqrexlemex  11551  resqrex  11552  sqrtdiv  11568  absvalsq  11579  absreimsq  11593  absdivap  11596  cau3lem  11640  maxabslemlub  11733  maxabslemval  11734  max0addsup  11745  minabs  11762  bdtrilem  11765  bdtri  11766  xrmaxaddlem  11786  xrmaxadd  11787  xrbdtri  11802  clim  11807  clim2  11809  climshftlemg  11828  climshft2  11832  climcn1  11834  climcn2  11835  subcn2  11837  reccn2ap  11839  climmulc2  11857  climsubc2  11859  clim2ser  11863  iser3shft  11872  climcau  11873  serf0  11878  fzosump1  11943  fsum1p  11944  fsump1  11946  sumsplitdc  11958  fsump1i  11959  mptfzshft  11968  fisum0diag2  11973  fsumconst  11980  fsumdifsnconst  11981  modfsummodlemstep  11983  modfsummod  11984  telfsumo  11992  fsumparts  11996  fsumrelem  11997  hash2iun1dif1  12006  binomlem  12009  binom  12010  binom1p  12011  binom1dif  12013  bcxmas  12015  isumsplit  12017  isum1p  12018  arisum  12024  arisum2  12025  trireciplem  12026  geoserap  12033  geolim  12037  geolim2  12038  georeclim  12039  geo2sum  12040  geoisum1  12045  cvgratnnlemseq  12052  cvgratnnlemsumlt  12054  cvgratnnlemfm  12055  cvgratz  12058  mertenslemi1  12061  mertenslem2  12062  mertensabs  12063  fprod1p  12125  fprodp1  12126  fprodcl2lem  12131  fprodfac  12141  fprodeq0  12143  fprodconst  12146  fprodrec  12155  fprodsplit1f  12160  fprodmodd  12167  efcllemp  12184  ef0lem  12186  efval  12187  esum  12188  ege2le3  12197  efaddlem  12200  efsep  12217  effsumlt  12218  eft0val  12219  efgt1p2  12221  efgt1p  12222  sinval  12228  cosval  12229  resinval  12241  recosval  12242  efi4p  12243  resin4p  12244  recos4p  12245  sinneg  12252  cosneg  12253  efival  12258  sinadd  12262  cosadd  12263  tanaddap  12265  sinmul  12270  cosmul  12271  cos2t  12276  cos2tsin  12277  ef01bndlem  12282  absefib  12297  demoivre  12299  demoivreALT  12300  eirraplem  12303  p1modz1  12320  dvdsmodexp  12321  moddvds  12325  mulmoddvds  12389  3dvds2dec  12392  zeo3  12394  odd2np1lem  12398  odd2np1  12399  oexpneg  12403  2tp1odd  12410  ltoddhalfle  12419  opoe  12421  opeo  12423  omeo  12424  m1expo  12426  m1exp1  12427  nn0o1gt2  12431  nn0o  12433  divalglemnn  12444  divalglemqt  12445  divalglemeunn  12447  divalglemex  12448  divalglemeuneg  12449  flodddiv4  12462  flodddiv4t2lthalf  12465  bitsp1o  12479  bitsmod  12482  bitsinv1lem  12487  gcdaddm  12520  bezoutlemnewy  12532  bezoutlema  12535  bezoutlemb  12536  bezoutlemex  12537  bezoutlemaz  12539  mulgcd  12552  gcddiv  12555  gcdmultiplez  12557  rpmulgcd  12562  rplpwr  12563  uzwodc  12573  lcmgcdlem  12614  lcmgcd  12615  divgcdcoprmex  12639  cncongr2  12641  prmexpb  12688  rpexp  12690  rpexp1i  12691  sqrt2irrlem  12698  oddpwdclemxy  12706  oddpwdclemndvds  12708  sqpweven  12712  2sqpwodd  12713  sqne2sq  12714  qmuldeneqnum  12732  nn0gcdsq  12737  zgcdsq  12738  numdensq  12739  dfphi2  12757  phiprmpw  12759  phiprm  12760  eulerthlema  12767  eulerthlemh  12768  eulerthlemth  12769  fermltl  12771  prmdiv  12772  prmdiveq  12773  prmdivdiv  12774  hashgcdlem  12775  odzval  12779  odzcllem  12780  odzdvds  12783  vfermltl  12789  powm2modprm  12790  reumodprminv  12791  modprm0  12792  nnnn0modprm0  12793  modprmn0modprm0  12794  coprimeprodsq  12795  coprimeprodsq2  12796  pythagtriplem1  12803  pythagtriplem3  12805  pythagtriplem4  12806  pythagtriplem6  12808  pythagtriplem7  12809  pythagtriplem12  12813  pythagtriplem14  12815  pythagtriplem15  12816  pythagtriplem16  12817  pythagtriplem17  12818  pythagtriplem18  12819  pceu  12833  pczpre  12835  pcdiv  12840  pcqdiv  12845  pcrec  12846  pczndvds  12854  pcneg  12863  pc2dvds  12868  pcprmpw2  12871  pcaddlem  12877  pcadd  12878  fldivp1  12886  pockthlem  12894  pockthi  12896  4sqlem5  12920  4sqlem9  12924  4sqlem10  12925  4sqlem2  12927  4sqlem3  12928  4sqlem4  12930  mul4sqlem  12931  4sqlem11  12939  4sqlem12  12940  4sqlem14  12942  4sqlem15  12943  4sqlem17  12945  4sqlem19  12947  ennnfonelemkh  12998  ennnfonelemhf1o  12999  setscomd  13088  ressressg  13123  qusex  13373  qusin  13374  grpinvalem  13433  grpinva  13434  grprida  13435  gsumsplit1r  13446  isnsgrp  13454  sgrpass  13456  sgrp1  13459  sgrppropd  13461  prdssgrpd  13463  mnd12g  13476  mndpropd  13488  prdsidlem  13495  prdsmndd  13496  imasmnd2  13500  mhmex  13510  mhmlin  13515  grprcan  13585  grpinvid1  13600  isgrpinv  13602  grplcan  13610  grpasscan1  13611  grplmulf1o  13622  grpinvadd  13626  grpinvsub  13630  grpsubsub4  13641  grppnpcan2  13642  grpnpncan  13643  dfgrp3mlem  13646  dfgrp3m  13647  grplactcnv  13650  prdsinvlem  13656  imasgrp2  13662  mhmlem  13666  mhmid  13667  mhmmnd  13668  mulgnnp1  13682  mulg2  13683  mulgnn0p1  13685  mulgsubcl  13688  mulgneg  13692  mulgaddcomlem  13697  mulgaddcom  13698  mulgz  13702  mulgnn0dir  13704  mulgdirlem  13705  mulgdir  13706  mulgneg2  13708  mulgnnass  13709  mulgnn0ass  13710  mulgass  13711  mulgassr  13712  mulgmodid  13713  mulgsubdir  13714  submmulg  13718  isnsg3  13759  nmzsubg  13762  ssnmz  13763  0nsg  13766  eqger  13776  eqgid  13778  eqgcpbl  13780  ghmlin  13800  ghmmulg  13808  ghmnsgima  13820  ghmnsgpreima  13821  conjghm  13828  conjnmz  13831  ablsub2inv  13863  abladdsub4  13866  abladdsub  13867  ablpncan2  13868  ablpnpcan  13872  ablnncan  13873  ablnnncan1  13876  gsumfzconst  13893  gsumfzsnfd  13897  mgpress  13909  rngass  13917  rngdi  13918  rngdir  13919  rnglz  13923  rngmneg1  13925  rngsubdir  13930  rngpropd  13933  imasrng  13934  srgass  13949  srgmulgass  13967  srgpcomp  13968  srgpcompp  13969  srgpcomppsc  13970  ringpropd  14016  ringlz  14021  ring1eq0  14026  ringnegl  14029  ringmneg1  14031  ringsubdir  14035  mulgass2  14036  ring1  14037  imasring  14042  opprrng  14055  opprring  14057  unitgrp  14095  dvrcan1  14119  rdivmuldivd  14123  subrginv  14216  resrhm  14227  unitrrg  14246  islmod  14270  lmodlema  14271  islmodd  14272  lmod0vs  14300  lmodvs0  14301  lmodvsmmulgdi  14302  lmodvneg1  14309  lmodvsneg  14310  lmodsubvs  14322  lmodsubdi  14323  lmodsubdir  14324  lmodprop2d  14327  rmodislmodlem  14329  rmodislmod  14330  lsssetm  14335  islssmd  14338  lssclg  14343  lssvacl  14344  lss1d  14362  lsspropdg  14410  sraval  14416  rnglidlmcl  14459  gsumfzfsumlemm  14566  znunit  14638  mplsubgfilemcl  14678  resttop  14859  restco  14863  restin  14865  lmfval  14882  cnprcl2k  14895  txrest  14965  txdis1cn  14967  cnmpt2res  14986  psmettri2  15017  psmettri  15019  xmettri2  15050  xmettri  15061  mettri  15062  metrtri  15066  blvalps  15077  blval  15078  xblss2  15094  blhalf  15097  comet  15188  xmetxp  15196  txmetcnp  15207  cnmet  15219  ioo2bl  15240  ivthreinc  15334  limcmpted  15352  limcimolemlt  15353  cnplimclemr  15358  limccnp2cntop  15366  reldvg  15368  dvfvalap  15370  dvidlemap  15380  dvidrelem  15381  dvidsslem  15382  dvconst  15383  dvconstre  15385  dvconstss  15387  dvcnp2cntop  15388  dvaddxxbr  15390  dvmulxxbr  15391  dvcoapbr  15396  dvcjbr  15397  dvexp  15400  dvrecap  15402  dvmptcmulcn  15410  dveflem  15415  plyval  15421  elply2  15424  elplyr  15429  elplyd  15430  ply1termlem  15431  plyaddlem1  15436  plymullem1  15437  plycoeid3  15446  plycjlemc  15449  dvply1  15454  sin0pilem1  15470  sinperlem  15497  ptolemy  15513  tangtx  15527  abssinper  15535  reexplog  15560  relogexp  15561  cxprec  15599  rpdivcxp  15600  cxpmul  15601  rpabscxpbnd  15629  rplogbval  15634  rplogbreexp  15642  rprelogbmul  15644  logbrec  15649  logbgcd1irraplemap  15658  binom4  15668  wilthlem1  15669  mpodvdsmulf1o  15679  sgmppw  15681  0sgmppw  15682  1sgmprm  15683  1sgm2ppw  15684  perfectlem1  15688  perfectlem2  15689  perfect  15690  lgslem1  15694  lgslem4  15697  lgsval  15698  lgsfvalg  15699  lgsval2lem  15704  lgsval4lem  15705  lgsvalmod  15713  lgsneg  15718  lgsneg1  15719  lgsmod  15720  lgsdilem  15721  lgsdir2lem4  15725  lgsdir2  15727  lgsdirprm  15728  lgsdir  15729  lgsne0  15732  lgssq  15734  lgssq2  15735  lgsmulsqcoprm  15740  lgsdirnn0  15741  lgsdinn0  15742  gausslemma2dlem1a  15752  gausslemma2dlem4  15758  gausslemma2dlem5a  15759  gausslemma2dlem5  15760  gausslemma2dlem6  15761  gausslemma2dlem7  15762  gausslemma2d  15763  lgseisenlem1  15764  lgseisenlem2  15765  lgseisenlem3  15766  lgseisenlem4  15767  lgseisen  15768  lgsquadlem1  15771  lgsquadlem2  15772  lgsquad2lem1  15775  lgsquad2lem2  15776  lgsquad3  15778  m1lgs  15779  2lgslem1a  15782  2lgslem1c  15784  2lgslem3a  15787  2lgslem3b  15788  2lgslem3c  15789  2lgslem3d  15790  2lgslem3a1  15791  2lgslem3b1  15792  2lgslem3c1  15793  2lgslem3d1  15794  2lgsoddprmlem1  15799  2lgsoddprmlem2  15800  2lgsoddprmlem3  15805  2sqlem1  15808  2sqlem2  15809  mul2sq  15810  2sqlem3  15811  2sqlem4  15812  2sqlem8  15817  2sqlem9  15818  2sqlem10  15819  uspgr2wlkeqi  16108  isclwwlk  16132  clwwlkccatlem  16137  trilpolemeq1  16468  trilpolemlt1  16469  trirec0xor  16473  apdifflemf  16474  apdiff  16476