Theorem oveq1d 6065

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 6057	. 2 ⊢ (𝐴 = 𝐵 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))
3	1, 2	syl 14	1 ⊢ (𝜑 → (𝐴𝐹𝐶) = (𝐵𝐹𝐶))

Syntax hints:   → wi 4   = wceq 1398  (class class class)co 6050

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-rex 2526  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-uni 3915  df-br 4110  df-iota 5312  df-fv 5360  df-ov 6053

This theorem is referenced by:  fvoveq1d  6072  csbov2g  6092  caovassg  6213  caovdig  6229  caovdirg  6232  caov12d  6236  caov31d  6237  caov411d  6240  caofinvl  6292  suppofss1dcl  6464  suppofss2dcl  6465  omsuc  6705  nnmsucr  6721  nnm1  6758  nnm2  6759  ecovass  6878  ecoviass  6879  ecovdi  6880  ecovidi  6881  isacnm  7510  addasspig  7645  mulasspig  7647  mulpipq2  7686  distrnqg  7702  ltsonq  7713  ltanqg  7715  ltmnqg  7716  ltexnqq  7723  archnqq  7732  prarloclemarch2  7734  enq0sym  7747  addnq0mo  7762  mulnq0mo  7763  addnnnq0  7764  nqpnq0nq  7768  nq0m0r  7771  nq0a0  7772  nnanq0  7773  distrnq0  7774  addassnq0  7777  addpinq1  7779  prarloclemlo  7809  prarloclem3  7812  prarloclem5  7815  prarloclemcalc  7817  addnqprllem  7842  addnqprulem  7843  appdivnq  7878  recexprlem1ssl  7948  recexprlem1ssu  7949  ltmprr  7957  cauappcvgprlemladdru  7971  cauappcvgprlem1  7974  caucvgprlemnkj  7981  caucvgprlemnbj  7982  caucvgprlemcl  7991  caucvgprlemladdfu  7992  caucvgprlemladdrl  7993  caucvgprlem1  7994  caucvgprprlemcbv  8002  caucvgprprlemval  8003  caucvgprprlemexb  8022  caucvgprprlem1  8024  addcmpblnr  8054  mulcmpblnrlemg  8055  addsrmo  8058  mulsrmo  8059  addsrpr  8060  mulsrpr  8061  ltsrprg  8062  1idsr  8083  pn0sr  8086  recexgt0sr  8088  mulgt0sr  8093  srpospr  8098  prsradd  8101  caucvgsrlemfv  8106  caucvgsrlemcau  8108  caucvgsrlemgt1  8110  caucvgsrlemoffval  8111  caucvgsrlemoffcau  8113  caucvgsrlemoffres  8115  caucvgsrlembnd  8116  caucvgsr  8117  map2psrprg  8120  pitonnlem1p1  8161  pitonnlem2  8162  pitonn  8163  recidpirqlemcalc  8172  ax1rid  8192  axrnegex  8194  axcnre  8196  recriota  8205  nntopi  8209  axcaucvglemval  8212  axcaucvglemcau  8213  axcaucvglemres  8214  mul12  8402  mul4  8405  muladd11  8406  readdcan  8413  muladd11r  8429  add12  8431  cnegex  8451  addcan  8453  negeu  8464  pncan2  8480  addsubass  8483  addsub  8484  2addsub  8487  addsubeq4  8488  subid  8492  subid1  8493  npncan  8494  nppcan  8495  nnpcan  8496  nnncan1  8509  npncan3  8511  pnpcan  8512  pnncan  8514  ppncan  8515  addsub4  8516  negsub  8521  subneg  8522  subeqxfrd  8636  mvlraddd  8637  mvlladdd  8638  mvrraddd  8639  subaddeqd  8642  ine0  8667  mulneg1  8668  ltadd2  8693  apreap  8861  cru  8876  recexap  8927  mulcanapd  8935  div23ap  8965  div13ap  8967  divmulassap  8969  divmulasscomap  8970  divcanap4  8973  muldivdirap  8981  divsubdirap  8982  divmuldivap  8986  divdivdivap  8987  divcanap5  8988  divmul13ap  8989  divmuleqap  8991  divdiv32ap  8994  divcanap7  8995  dmdcanap  8996  divdivap1  8997  divdivap2  8998  divadddivap  9001  divsubdivap  9002  conjmulap  9003  divneg2ap  9010  subrecap  9113  mvllmulapd  9116  lt2mul2div  9153  nndivtr  9279  2halves  9467  halfaddsub  9472  subhalfhalf  9473  avgle1  9479  avgle2  9480  div4p1lem1div2  9492  un0addcl  9529  un0mulcl  9530  peano2z  9613  zneo  9679  nneoor  9680  nneo  9681  zeo  9683  zeo2  9684  deceq1  9713  qreccl  9974  xaddcom  10194  xnegdi  10201  xaddass  10202  xaddass2  10203  xpncan  10204  xleadd1a  10206  xltadd1  10209  xposdif  10215  xadd4d  10218  lincmb01cmp  10336  lincmble  10337  iccf1o  10338  fz0to4untppr  10458  fzo0addel  10533  fzosubel3  10541  qavgle  10618  2tnp1ge0ge0  10661  fldiv4p1lem1div2  10665  fldiv4lem1div2  10667  ceilqm1lt  10674  flqdiv  10683  modqlt  10695  modqdiffl  10697  modqcyc2  10722  modqaddabs  10724  mulqaddmodid  10726  mulp1mod1  10727  modqmuladd  10728  modqmuladdnn0  10730  qnegmod  10731  addmodid  10734  addmodidr  10735  modqadd2mod  10736  modqm1p1mod0  10737  modqmul12d  10740  modqnegd  10741  modqadd12d  10742  modqsub12d  10743  q2submod  10747  modqmulmodr  10752  modqaddmulmod  10753  modqsubdir  10755  modfzo0difsn  10757  modsumfzodifsn  10758  addmodlteq  10760  frecuzrdgsuc  10776  frecfzennn  10788  iseqovex  10820  seq3-1p  10852  seq3caopr2  10855  seqcaopr2g  10856  seq3caopr  10857  seqcaoprg  10858  seqf1oglem2a  10880  seqf1oglem1  10881  seqf1oglem2  10882  seq3id  10887  seq3homo  10889  seq3z  10890  seqhomog  10892  seqfeq4g  10893  expp1  10908  exprecap  10942  expaddzaplem  10944  expmulzap  10947  expdivap  10952  sqval  10959  sqsubswap  10961  sqdividap  10966  subsq  11008  subsq2  11009  binom2  11013  binom2sub  11015  mulbinom2  11018  binom3  11019  zesq  11020  bernneq2  11023  modqexp  11028  sqoddm1div8  11055  mulsubdivbinom2ap  11073  nn0opthlem1d  11082  nn0opthd  11084  nn0opth2d  11085  facp1  11092  facdiv  11100  facndiv  11101  faclbnd  11103  faclbnd2  11104  faclbnd3  11105  bcval  11111  bccmpl  11116  bcm1k  11122  bcp1n  11123  bcp1nk  11124  bcval5  11125  bcp1m1  11127  bcpasc  11128  bcm1n  11131  bcn2m1  11132  hashprg  11173  hashdifpr  11185  hashfzo  11187  hashfzp1  11189  hashfz0  11190  hashxp  11191  hashfibclem  11206  hashfibc  11207  zfz1isolemsplit  11210  zfz1isolem1  11212  seq3coll  11214  lswwrd  11271  ccatfvalfi  11280  ccatass  11296  lswccatn0lsw  11299  wrdlenccats1lenm1g  11324  ccatw2s1leng  11326  ccatswrd  11362  ccatpfx  11393  swrdpfx  11399  pfxpfx  11400  ccats1pfxeq  11406  wrdeqs1cat  11412  wrdind  11414  wrd2ind  11415  pfxccatpfx2  11429  pfxccatin12d  11437  cats1catd  11460  cats2catd  11461  s2leng  11481  s3s4d  11495  s2s5d  11496  s5s2d  11497  reval  11534  crre  11542  remim  11545  remul2  11558  immul2  11565  imval2  11579  cjdivap  11594  caucvgre  11666  cvg1nlemcau  11669  cvg1nlemres  11670  resqrexlemp1rp  11691  resqrexlemfp1  11694  resqrexlemover  11695  resqrexlemcalc1  11699  resqrexlemcalc3  11701  resqrexlemnm  11703  resqrexlemoverl  11706  resqrexlemglsq  11707  resqrexlemga  11708  resqrexlemsqa  11709  resqrexlemex  11710  resqrex  11711  sqrtdiv  11727  absvalsq  11738  absreimsq  11752  absdivap  11755  cau3lem  11799  maxabslemlub  11892  maxabslemval  11893  max0addsup  11904  minabs  11921  bdtrilem  11924  bdtri  11925  xrmaxaddlem  11945  xrmaxadd  11946  xrbdtri  11961  clim  11966  clim2  11968  climshftlemg  11987  climshft2  11991  climcn1  11993  climcn2  11994  subcn2  11996  reccn2ap  11998  climmulc2  12016  climsubc2  12018  clim2ser  12022  iser3shft  12031  climcau  12032  serf0  12037  fzosump1  12103  fsum1p  12104  fsump1  12106  sumsplitdc  12118  fsump1i  12119  mptfzshft  12128  fisum0diag2  12133  fsumconst  12140  fsumdifsnconst  12141  modfsummodlemstep  12143  modfsummod  12144  telfsumo  12152  fsumparts  12156  fsumrelem  12157  hash2iun1dif1  12166  binomlem  12169  binom  12170  binom1p  12171  binom1dif  12173  bcxmas  12175  isumsplit  12177  isum1p  12178  arisum  12184  arisum2  12185  trireciplem  12186  geoserap  12193  geolim  12197  geolim2  12198  georeclim  12199  geo2sum  12200  geoisum1  12205  cvgratnnlemseq  12212  cvgratnnlemsumlt  12214  cvgratnnlemfm  12215  cvgratz  12218  mertenslemi1  12221  mertenslem2  12222  mertensabs  12223  fprod1p  12285  fprodp1  12286  fprodcl2lem  12291  fprodfac  12301  fprodeq0  12303  fprodconst  12306  fprodrec  12315  fprodsplit1f  12320  fprodmodd  12327  efcllemp  12344  ef0lem  12346  efval  12347  esum  12348  ege2le3  12357  efaddlem  12360  efsep  12377  effsumlt  12378  eft0val  12379  efgt1p2  12381  efgt1p  12382  sinval  12388  cosval  12389  resinval  12401  recosval  12402  efi4p  12403  resin4p  12404  recos4p  12405  sinneg  12412  cosneg  12413  efival  12418  sinadd  12422  cosadd  12423  tanaddap  12425  sinmul  12430  cosmul  12431  cos2t  12436  cos2tsin  12437  ef01bndlem  12442  absefib  12457  demoivre  12459  demoivreALT  12460  eirraplem  12463  p1modz1  12480  dvdsmodexp  12481  moddvds  12485  mulmoddvds  12549  3dvds2dec  12552  zeo3  12554  odd2np1lem  12558  odd2np1  12559  oexpneg  12563  2tp1odd  12570  ltoddhalfle  12579  opoe  12581  opeo  12583  omeo  12584  m1expo  12586  m1exp1  12587  nn0o1gt2  12591  nn0o  12593  divalglemnn  12604  divalglemqt  12605  divalglemeunn  12607  divalglemex  12608  divalglemeuneg  12609  flodddiv4  12622  flodddiv4t2lthalf  12625  bitsp1o  12639  bitsmod  12642  bitsinv1lem  12647  gcdaddm  12680  bezoutlemnewy  12692  bezoutlema  12695  bezoutlemb  12696  bezoutlemex  12697  bezoutlemaz  12699  mulgcd  12712  gcddiv  12715  gcdmultiplez  12717  rpmulgcd  12722  rplpwr  12723  uzwodc  12733  lcmgcdlem  12774  lcmgcd  12775  divgcdcoprmex  12799  cncongr2  12801  prmexpb  12848  rpexp  12850  rpexp1i  12851  sqrt2irrlem  12858  oddpwdclemxy  12866  oddpwdclemndvds  12868  sqpweven  12872  2sqpwodd  12873  sqne2sq  12874  qmuldeneqnum  12892  nn0gcdsq  12897  zgcdsq  12898  numdensq  12899  dfphi2  12917  phiprmpw  12919  phiprm  12920  eulerthlema  12927  eulerthlemh  12928  eulerthlemth  12929  fermltl  12931  prmdiv  12932  prmdiveq  12933  prmdivdiv  12934  hashgcdlem  12935  odzval  12939  odzcllem  12940  odzdvds  12943  vfermltl  12949  powm2modprm  12950  reumodprminv  12951  modprm0  12952  nnnn0modprm0  12953  modprmn0modprm0  12954  coprimeprodsq  12955  coprimeprodsq2  12956  pythagtriplem1  12963  pythagtriplem3  12965  pythagtriplem4  12966  pythagtriplem6  12968  pythagtriplem7  12969  pythagtriplem12  12973  pythagtriplem14  12975  pythagtriplem15  12976  pythagtriplem16  12977  pythagtriplem17  12978  pythagtriplem18  12979  pceu  12993  pczpre  12995  pcdiv  13000  pcqdiv  13005  pcrec  13006  pczndvds  13014  pcneg  13023  pc2dvds  13028  pcprmpw2  13031  pcaddlem  13037  pcadd  13038  fldivp1  13046  pockthlem  13054  pockthi  13056  4sqlem5  13080  4sqlem9  13084  4sqlem10  13085  4sqlem2  13087  4sqlem3  13088  4sqlem4  13090  mul4sqlem  13091  4sqlem11  13099  4sqlem12  13100  4sqlem14  13102  4sqlem15  13103  4sqlem17  13105  4sqlem19  13107  ballotfilem2  13142  ennnfonelemkh  13163  ennnfonelemhf1o  13164  setscomd  13253  ressressg  13288  qusex  13538  qusin  13539  grpinvalem  13598  grpinva  13599  grprida  13600  gsumsplit1r  13611  isnsgrp  13619  sgrpass  13621  sgrp1  13624  sgrppropd  13626  prdssgrpd  13628  mnd12g  13641  mndpropd  13653  prdsidlem  13660  prdsmndd  13661  imasmnd2  13665  mhmex  13675  mhmlin  13680  grprcan  13750  grpinvid1  13765  isgrpinv  13767  grplcan  13775  grpasscan1  13776  grplmulf1o  13787  grpinvadd  13791  grpinvsub  13795  grpsubsub4  13806  grppnpcan2  13807  grpnpncan  13808  dfgrp3mlem  13811  dfgrp3m  13812  grplactcnv  13815  prdsinvlem  13821  imasgrp2  13827  mhmlem  13831  mhmid  13832  mhmmnd  13833  mulgnnp1  13847  mulg2  13848  mulgnn0p1  13850  mulgsubcl  13853  mulgneg  13857  mulgaddcomlem  13862  mulgaddcom  13863  mulgz  13867  mulgnn0dir  13869  mulgdirlem  13870  mulgdir  13871  mulgneg2  13873  mulgnnass  13874  mulgnn0ass  13875  mulgass  13876  mulgassr  13877  mulgmodid  13878  mulgsubdir  13879  submmulg  13883  isnsg3  13924  nmzsubg  13927  ssnmz  13928  0nsg  13931  eqger  13941  eqgid  13943  eqgcpbl  13945  ghmlin  13965  ghmmulg  13973  ghmnsgima  13985  ghmnsgpreima  13986  conjghm  13993  conjnmz  13996  ablsub2inv  14028  abladdsub4  14031  abladdsub  14032  ablpncan2  14033  ablpnpcan  14037  ablnncan  14038  ablnnncan1  14041  gsumfzconst  14058  gsumfzsnfd  14062  gsumsplit0  14063  mgpress  14075  rngass  14083  rngdi  14084  rngdir  14085  rnglz  14089  rngmneg1  14091  rngsubdir  14096  rngpropd  14099  imasrng  14100  srgass  14115  srgmulgass  14133  srgpcomp  14134  srgpcompp  14135  srgpcomppsc  14136  ringpropd  14182  ringlz  14187  ring1eq0  14192  ringnegl  14195  ringmneg1  14197  ringsubdir  14201  mulgass2  14202  ring1  14203  imasring  14208  opprrng  14221  opprring  14223  unitgrp  14261  dvrcan1  14285  rdivmuldivd  14289  subrginv  14382  resrhm  14393  unitrrg  14413  aprlring  14434  islmod  14439  lmodlema  14440  islmodd  14441  lmod0vs  14469  lmodvs0  14470  lmodvsmmulgdi  14471  lmodvneg1  14478  lmodvsneg  14479  lmodsubvs  14491  lmodsubdi  14492  lmodsubdir  14493  lmodprop2d  14496  rmodislmodlem  14498  rmodislmod  14499  lsssetm  14504  islssmd  14507  lssclg  14512  lssvacl  14513  lss1d  14531  lsspropdg  14579  sraval  14585  rnglidlmcl  14628  gsumfzfsumlemm  14735  znunit  14807  mplsubgfilemcl  14854  resttop  15035  restco  15039  restin  15041  lmfval  15058  cnprcl2k  15071  txrest  15141  txdis1cn  15143  cnmpt2res  15162  psmettri2  15193  psmettri  15195  xmettri2  15226  xmettri  15237  mettri  15238  metrtri  15242  blvalps  15253  blval  15254  xblss2  15270  blhalf  15273  comet  15364  xmetxp  15372  txmetcnp  15383  cnmet  15395  ioo2bl  15416  ivthreinc  15510  limcmpted  15528  limcimolemlt  15529  cnplimclemr  15534  limccnp2cntop  15542  reldvg  15544  dvfvalap  15546  dvidlemap  15556  dvidrelem  15557  dvidsslem  15558  dvconst  15559  dvconstre  15561  dvconstss  15563  dvcnp2cntop  15564  dvaddxxbr  15566  dvmulxxbr  15567  dvcoapbr  15572  dvcjbr  15573  dvexp  15576  dvrecap  15578  dvmptcmulcn  15586  dveflem  15591  plyval  15597  elply2  15600  elplyr  15605  elplyd  15606  ply1termlem  15607  plyaddlem1  15612  plymullem1  15613  plycoeid3  15622  plycjlemc  15625  dvply1  15630  sin0pilem1  15646  sinperlem  15673  ptolemy  15689  tangtx  15703  abssinper  15711  reexplog  15736  relogexp  15737  cxprec  15775  rpdivcxp  15776  cxpmul  15777  rpabscxpbnd  15805  rplogbval  15810  rplogbreexp  15818  rprelogbmul  15820  logbrec  15825  logbgcd1irraplemap  15834  binom4  15844  pellexlem2  15846  pellexlem3  15847  wilthlem1  15848  mpodvdsmulf1o  15858  sgmppw  15860  0sgmppw  15861  1sgmprm  15862  1sgm2ppw  15863  perfectlem1  15867  perfectlem2  15868  perfect  15869  lgslem1  15873  lgslem4  15876  lgsval  15877  lgsfvalg  15878  lgsval2lem  15883  lgsval4lem  15884  lgsvalmod  15892  lgsneg  15897  lgsneg1  15898  lgsmod  15899  lgsdilem  15900  lgsdir2lem4  15904  lgsdir2  15906  lgsdirprm  15907  lgsdir  15908  lgsne0  15911  lgssq  15913  lgssq2  15914  lgsmulsqcoprm  15919  lgsdirnn0  15920  lgsdinn0  15921  gausslemma2dlem1a  15931  gausslemma2dlem4  15937  gausslemma2dlem5a  15938  gausslemma2dlem5  15939  gausslemma2dlem6  15940  gausslemma2dlem7  15941  gausslemma2d  15942  lgseisenlem1  15943  lgseisenlem2  15944  lgseisenlem3  15945  lgseisenlem4  15946  lgseisen  15947  lgsquadlem1  15950  lgsquadlem2  15951  lgsquad2lem1  15954  lgsquad2lem2  15955  lgsquad3  15957  m1lgs  15958  2lgslem1a  15961  2lgslem1c  15963  2lgslem3a  15966  2lgslem3b  15967  2lgslem3c  15968  2lgslem3d  15969  2lgslem3a1  15970  2lgslem3b1  15971  2lgslem3c1  15972  2lgslem3d1  15973  2lgsoddprmlem1  15978  2lgsoddprmlem2  15979  2lgsoddprmlem3  15984  2sqlem1  15987  2sqlem2  15988  mul2sq  15989  2sqlem3  15990  2sqlem4  15991  2sqlem8  15996  2sqlem9  15997  2sqlem10  15998  vdegp1bid  16310  uspgr2wlkeqi  16362  isclwwlk  16389  clwwlkccatlem  16395  clwwlknonex2  16434  repiecele0  16810  repiecege0  16811  repiecef  16812  trilpolemeq1  16824  trilpolemlt1  16825  trirec0xor  16829  apdifflemf  16830  apdiff  16832  qdiff  16833  gsumgfsumlem  16865  gsumgfsum  16866