Theorem oveq1d 6033

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

Syntax hints:   → wi 4   = wceq 1397  (class class class)co 6018

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6021

This theorem is referenced by:  fvoveq1d  6040  csbov2g  6060  caovassg  6181  caovdig  6197  caovdirg  6200  caov12d  6204  caov31d  6205  caov411d  6208  caofinvl  6261  omsuc  6640  nnmsucr  6656  nnm1  6693  nnm2  6694  ecovass  6813  ecoviass  6814  ecovdi  6815  ecovidi  6816  isacnm  7418  addasspig  7550  mulasspig  7552  mulpipq2  7591  distrnqg  7607  ltsonq  7618  ltanqg  7620  ltmnqg  7621  ltexnqq  7628  archnqq  7637  prarloclemarch2  7639  enq0sym  7652  addnq0mo  7667  mulnq0mo  7668  addnnnq0  7669  nqpnq0nq  7673  nq0m0r  7676  nq0a0  7677  nnanq0  7678  distrnq0  7679  addassnq0  7682  addpinq1  7684  prarloclemlo  7714  prarloclem3  7717  prarloclem5  7720  prarloclemcalc  7722  addnqprllem  7747  addnqprulem  7748  appdivnq  7783  recexprlem1ssl  7853  recexprlem1ssu  7854  ltmprr  7862  cauappcvgprlemladdru  7876  cauappcvgprlem1  7879  caucvgprlemnkj  7886  caucvgprlemnbj  7887  caucvgprlemcl  7896  caucvgprlemladdfu  7897  caucvgprlemladdrl  7898  caucvgprlem1  7899  caucvgprprlemcbv  7907  caucvgprprlemval  7908  caucvgprprlemexb  7927  caucvgprprlem1  7929  addcmpblnr  7959  mulcmpblnrlemg  7960  addsrmo  7963  mulsrmo  7964  addsrpr  7965  mulsrpr  7966  ltsrprg  7967  1idsr  7988  pn0sr  7991  recexgt0sr  7993  mulgt0sr  7998  srpospr  8003  prsradd  8006  caucvgsrlemfv  8011  caucvgsrlemcau  8013  caucvgsrlemgt1  8015  caucvgsrlemoffval  8016  caucvgsrlemoffcau  8018  caucvgsrlemoffres  8020  caucvgsrlembnd  8021  caucvgsr  8022  map2psrprg  8025  pitonnlem1p1  8066  pitonnlem2  8067  pitonn  8068  recidpirqlemcalc  8077  ax1rid  8097  axrnegex  8099  axcnre  8101  recriota  8110  nntopi  8114  axcaucvglemval  8117  axcaucvglemcau  8118  axcaucvglemres  8119  mul12  8308  mul4  8311  muladd11  8312  readdcan  8319  muladd11r  8335  add12  8337  cnegex  8357  addcan  8359  negeu  8370  pncan2  8386  addsubass  8389  addsub  8390  2addsub  8393  addsubeq4  8394  subid  8398  subid1  8399  npncan  8400  nppcan  8401  nnpcan  8402  nnncan1  8415  npncan3  8417  pnpcan  8418  pnncan  8420  ppncan  8421  addsub4  8422  negsub  8427  subneg  8428  subeqxfrd  8542  mvlraddd  8543  mvlladdd  8544  mvrraddd  8545  subaddeqd  8548  ine0  8573  mulneg1  8574  ltadd2  8599  apreap  8767  cru  8782  recexap  8833  mulcanapd  8841  div23ap  8871  div13ap  8873  divmulassap  8875  divmulasscomap  8876  divcanap4  8879  muldivdirap  8887  divsubdirap  8888  divmuldivap  8892  divdivdivap  8893  divcanap5  8894  divmul13ap  8895  divmuleqap  8897  divdiv32ap  8900  divcanap7  8901  dmdcanap  8902  divdivap1  8903  divdivap2  8904  divadddivap  8907  divsubdivap  8908  conjmulap  8909  divneg2ap  8916  subrecap  9019  mvllmulapd  9022  lt2mul2div  9059  nndivtr  9185  2halves  9373  halfaddsub  9378  subhalfhalf  9379  avgle1  9385  avgle2  9386  div4p1lem1div2  9398  un0addcl  9435  un0mulcl  9436  peano2z  9515  zneo  9581  nneoor  9582  nneo  9583  zeo  9585  zeo2  9586  deceq1  9615  qreccl  9876  xaddcom  10096  xnegdi  10103  xaddass  10104  xaddass2  10105  xpncan  10106  xleadd1a  10108  xltadd1  10111  xposdif  10117  xadd4d  10120  lincmb01cmp  10238  iccf1o  10239  fz0to4untppr  10359  fzo0addel  10434  fzosubel3  10442  qavgle  10519  2tnp1ge0ge0  10562  fldiv4p1lem1div2  10566  fldiv4lem1div2  10568  ceilqm1lt  10575  flqdiv  10584  modqlt  10596  modqdiffl  10598  modqcyc2  10623  modqaddabs  10625  mulqaddmodid  10627  mulp1mod1  10628  modqmuladd  10629  modqmuladdnn0  10631  qnegmod  10632  addmodid  10635  addmodidr  10636  modqadd2mod  10637  modqm1p1mod0  10638  modqmul12d  10641  modqnegd  10642  modqadd12d  10643  modqsub12d  10644  q2submod  10648  modqmulmodr  10653  modqaddmulmod  10654  modqsubdir  10656  modfzo0difsn  10658  modsumfzodifsn  10659  addmodlteq  10661  frecuzrdgsuc  10677  frecfzennn  10689  iseqovex  10721  seq3-1p  10753  seq3caopr2  10756  seqcaopr2g  10757  seq3caopr  10758  seqcaoprg  10759  seqf1oglem2a  10781  seqf1oglem1  10782  seqf1oglem2  10783  seq3id  10788  seq3homo  10790  seq3z  10791  seqhomog  10793  seqfeq4g  10794  expp1  10809  exprecap  10843  expaddzaplem  10845  expmulzap  10848  expdivap  10853  sqval  10860  sqsubswap  10862  sqdividap  10867  subsq  10909  subsq2  10910  binom2  10914  binom2sub  10916  mulbinom2  10919  binom3  10920  zesq  10921  bernneq2  10924  modqexp  10929  sqoddm1div8  10956  mulsubdivbinom2ap  10974  nn0opthlem1d  10983  nn0opthd  10985  nn0opth2d  10986  facp1  10993  facdiv  11001  facndiv  11002  faclbnd  11004  faclbnd2  11005  faclbnd3  11006  bcval  11012  bccmpl  11017  bcm1k  11023  bcp1n  11024  bcp1nk  11025  bcval5  11026  bcp1m1  11028  bcpasc  11029  bcn2m1  11032  hashprg  11073  hashdifpr  11085  hashfzo  11087  hashfzp1  11089  hashfz0  11090  hashxp  11091  zfz1isolemsplit  11103  zfz1isolem1  11105  seq3coll  11107  lswwrd  11164  ccatfvalfi  11173  ccatass  11189  lswccatn0lsw  11192  wrdlenccats1lenm1g  11217  ccatw2s1leng  11219  ccatswrd  11255  ccatpfx  11286  swrdpfx  11292  pfxpfx  11293  ccats1pfxeq  11299  wrdeqs1cat  11305  wrdind  11307  wrd2ind  11308  pfxccatpfx2  11322  pfxccatin12d  11330  cats1catd  11353  cats2catd  11354  s2leng  11374  s3s4d  11388  s2s5d  11389  s5s2d  11390  reval  11427  crre  11435  remim  11438  remul2  11451  immul2  11458  imval2  11472  cjdivap  11487  caucvgre  11559  cvg1nlemcau  11562  cvg1nlemres  11563  resqrexlemp1rp  11584  resqrexlemfp1  11587  resqrexlemover  11588  resqrexlemcalc1  11592  resqrexlemcalc3  11594  resqrexlemnm  11596  resqrexlemoverl  11599  resqrexlemglsq  11600  resqrexlemga  11601  resqrexlemsqa  11602  resqrexlemex  11603  resqrex  11604  sqrtdiv  11620  absvalsq  11631  absreimsq  11645  absdivap  11648  cau3lem  11692  maxabslemlub  11785  maxabslemval  11786  max0addsup  11797  minabs  11814  bdtrilem  11817  bdtri  11818  xrmaxaddlem  11838  xrmaxadd  11839  xrbdtri  11854  clim  11859  clim2  11861  climshftlemg  11880  climshft2  11884  climcn1  11886  climcn2  11887  subcn2  11889  reccn2ap  11891  climmulc2  11909  climsubc2  11911  clim2ser  11915  iser3shft  11924  climcau  11925  serf0  11930  fzosump1  11996  fsum1p  11997  fsump1  11999  sumsplitdc  12011  fsump1i  12012  mptfzshft  12021  fisum0diag2  12026  fsumconst  12033  fsumdifsnconst  12034  modfsummodlemstep  12036  modfsummod  12037  telfsumo  12045  fsumparts  12049  fsumrelem  12050  hash2iun1dif1  12059  binomlem  12062  binom  12063  binom1p  12064  binom1dif  12066  bcxmas  12068  isumsplit  12070  isum1p  12071  arisum  12077  arisum2  12078  trireciplem  12079  geoserap  12086  geolim  12090  geolim2  12091  georeclim  12092  geo2sum  12093  geoisum1  12098  cvgratnnlemseq  12105  cvgratnnlemsumlt  12107  cvgratnnlemfm  12108  cvgratz  12111  mertenslemi1  12114  mertenslem2  12115  mertensabs  12116  fprod1p  12178  fprodp1  12179  fprodcl2lem  12184  fprodfac  12194  fprodeq0  12196  fprodconst  12199  fprodrec  12208  fprodsplit1f  12213  fprodmodd  12220  efcllemp  12237  ef0lem  12239  efval  12240  esum  12241  ege2le3  12250  efaddlem  12253  efsep  12270  effsumlt  12271  eft0val  12272  efgt1p2  12274  efgt1p  12275  sinval  12281  cosval  12282  resinval  12294  recosval  12295  efi4p  12296  resin4p  12297  recos4p  12298  sinneg  12305  cosneg  12306  efival  12311  sinadd  12315  cosadd  12316  tanaddap  12318  sinmul  12323  cosmul  12324  cos2t  12329  cos2tsin  12330  ef01bndlem  12335  absefib  12350  demoivre  12352  demoivreALT  12353  eirraplem  12356  p1modz1  12373  dvdsmodexp  12374  moddvds  12378  mulmoddvds  12442  3dvds2dec  12445  zeo3  12447  odd2np1lem  12451  odd2np1  12452  oexpneg  12456  2tp1odd  12463  ltoddhalfle  12472  opoe  12474  opeo  12476  omeo  12477  m1expo  12479  m1exp1  12480  nn0o1gt2  12484  nn0o  12486  divalglemnn  12497  divalglemqt  12498  divalglemeunn  12500  divalglemex  12501  divalglemeuneg  12502  flodddiv4  12515  flodddiv4t2lthalf  12518  bitsp1o  12532  bitsmod  12535  bitsinv1lem  12540  gcdaddm  12573  bezoutlemnewy  12585  bezoutlema  12588  bezoutlemb  12589  bezoutlemex  12590  bezoutlemaz  12592  mulgcd  12605  gcddiv  12608  gcdmultiplez  12610  rpmulgcd  12615  rplpwr  12616  uzwodc  12626  lcmgcdlem  12667  lcmgcd  12668  divgcdcoprmex  12692  cncongr2  12694  prmexpb  12741  rpexp  12743  rpexp1i  12744  sqrt2irrlem  12751  oddpwdclemxy  12759  oddpwdclemndvds  12761  sqpweven  12765  2sqpwodd  12766  sqne2sq  12767  qmuldeneqnum  12785  nn0gcdsq  12790  zgcdsq  12791  numdensq  12792  dfphi2  12810  phiprmpw  12812  phiprm  12813  eulerthlema  12820  eulerthlemh  12821  eulerthlemth  12822  fermltl  12824  prmdiv  12825  prmdiveq  12826  prmdivdiv  12827  hashgcdlem  12828  odzval  12832  odzcllem  12833  odzdvds  12836  vfermltl  12842  powm2modprm  12843  reumodprminv  12844  modprm0  12845  nnnn0modprm0  12846  modprmn0modprm0  12847  coprimeprodsq  12848  coprimeprodsq2  12849  pythagtriplem1  12856  pythagtriplem3  12858  pythagtriplem4  12859  pythagtriplem6  12861  pythagtriplem7  12862  pythagtriplem12  12866  pythagtriplem14  12868  pythagtriplem15  12869  pythagtriplem16  12870  pythagtriplem17  12871  pythagtriplem18  12872  pceu  12886  pczpre  12888  pcdiv  12893  pcqdiv  12898  pcrec  12899  pczndvds  12907  pcneg  12916  pc2dvds  12921  pcprmpw2  12924  pcaddlem  12930  pcadd  12931  fldivp1  12939  pockthlem  12947  pockthi  12949  4sqlem5  12973  4sqlem9  12977  4sqlem10  12978  4sqlem2  12980  4sqlem3  12981  4sqlem4  12983  mul4sqlem  12984  4sqlem11  12992  4sqlem12  12993  4sqlem14  12995  4sqlem15  12996  4sqlem17  12998  4sqlem19  13000  ennnfonelemkh  13051  ennnfonelemhf1o  13052  setscomd  13141  ressressg  13176  qusex  13426  qusin  13427  grpinvalem  13486  grpinva  13487  grprida  13488  gsumsplit1r  13499  isnsgrp  13507  sgrpass  13509  sgrp1  13512  sgrppropd  13514  prdssgrpd  13516  mnd12g  13529  mndpropd  13541  prdsidlem  13548  prdsmndd  13549  imasmnd2  13553  mhmex  13563  mhmlin  13568  grprcan  13638  grpinvid1  13653  isgrpinv  13655  grplcan  13663  grpasscan1  13664  grplmulf1o  13675  grpinvadd  13679  grpinvsub  13683  grpsubsub4  13694  grppnpcan2  13695  grpnpncan  13696  dfgrp3mlem  13699  dfgrp3m  13700  grplactcnv  13703  prdsinvlem  13709  imasgrp2  13715  mhmlem  13719  mhmid  13720  mhmmnd  13721  mulgnnp1  13735  mulg2  13736  mulgnn0p1  13738  mulgsubcl  13741  mulgneg  13745  mulgaddcomlem  13750  mulgaddcom  13751  mulgz  13755  mulgnn0dir  13757  mulgdirlem  13758  mulgdir  13759  mulgneg2  13761  mulgnnass  13762  mulgnn0ass  13763  mulgass  13764  mulgassr  13765  mulgmodid  13766  mulgsubdir  13767  submmulg  13771  isnsg3  13812  nmzsubg  13815  ssnmz  13816  0nsg  13819  eqger  13829  eqgid  13831  eqgcpbl  13833  ghmlin  13853  ghmmulg  13861  ghmnsgima  13873  ghmnsgpreima  13874  conjghm  13881  conjnmz  13884  ablsub2inv  13916  abladdsub4  13919  abladdsub  13920  ablpncan2  13921  ablpnpcan  13925  ablnncan  13926  ablnnncan1  13929  gsumfzconst  13946  gsumfzsnfd  13950  gsumsplit0  13951  mgpress  13963  rngass  13971  rngdi  13972  rngdir  13973  rnglz  13977  rngmneg1  13979  rngsubdir  13984  rngpropd  13987  imasrng  13988  srgass  14003  srgmulgass  14021  srgpcomp  14022  srgpcompp  14023  srgpcomppsc  14024  ringpropd  14070  ringlz  14075  ring1eq0  14080  ringnegl  14083  ringmneg1  14085  ringsubdir  14089  mulgass2  14090  ring1  14091  imasring  14096  opprrng  14109  opprring  14111  unitgrp  14149  dvrcan1  14173  rdivmuldivd  14177  subrginv  14270  resrhm  14281  unitrrg  14300  islmod  14324  lmodlema  14325  islmodd  14326  lmod0vs  14354  lmodvs0  14355  lmodvsmmulgdi  14356  lmodvneg1  14363  lmodvsneg  14364  lmodsubvs  14376  lmodsubdi  14377  lmodsubdir  14378  lmodprop2d  14381  rmodislmodlem  14383  rmodislmod  14384  lsssetm  14389  islssmd  14392  lssclg  14397  lssvacl  14398  lss1d  14416  lsspropdg  14464  sraval  14470  rnglidlmcl  14513  gsumfzfsumlemm  14620  znunit  14692  mplsubgfilemcl  14732  resttop  14913  restco  14917  restin  14919  lmfval  14936  cnprcl2k  14949  txrest  15019  txdis1cn  15021  cnmpt2res  15040  psmettri2  15071  psmettri  15073  xmettri2  15104  xmettri  15115  mettri  15116  metrtri  15120  blvalps  15131  blval  15132  xblss2  15148  blhalf  15151  comet  15242  xmetxp  15250  txmetcnp  15261  cnmet  15273  ioo2bl  15294  ivthreinc  15388  limcmpted  15406  limcimolemlt  15407  cnplimclemr  15412  limccnp2cntop  15420  reldvg  15422  dvfvalap  15424  dvidlemap  15434  dvidrelem  15435  dvidsslem  15436  dvconst  15437  dvconstre  15439  dvconstss  15441  dvcnp2cntop  15442  dvaddxxbr  15444  dvmulxxbr  15445  dvcoapbr  15450  dvcjbr  15451  dvexp  15454  dvrecap  15456  dvmptcmulcn  15464  dveflem  15469  plyval  15475  elply2  15478  elplyr  15483  elplyd  15484  ply1termlem  15485  plyaddlem1  15490  plymullem1  15491  plycoeid3  15500  plycjlemc  15503  dvply1  15508  sin0pilem1  15524  sinperlem  15551  ptolemy  15567  tangtx  15581  abssinper  15589  reexplog  15614  relogexp  15615  cxprec  15653  rpdivcxp  15654  cxpmul  15655  rpabscxpbnd  15683  rplogbval  15688  rplogbreexp  15696  rprelogbmul  15698  logbrec  15703  logbgcd1irraplemap  15712  binom4  15722  wilthlem1  15723  mpodvdsmulf1o  15733  sgmppw  15735  0sgmppw  15736  1sgmprm  15737  1sgm2ppw  15738  perfectlem1  15742  perfectlem2  15743  perfect  15744  lgslem1  15748  lgslem4  15751  lgsval  15752  lgsfvalg  15753  lgsval2lem  15758  lgsval4lem  15759  lgsvalmod  15767  lgsneg  15772  lgsneg1  15773  lgsmod  15774  lgsdilem  15775  lgsdir2lem4  15779  lgsdir2  15781  lgsdirprm  15782  lgsdir  15783  lgsne0  15786  lgssq  15788  lgssq2  15789  lgsmulsqcoprm  15794  lgsdirnn0  15795  lgsdinn0  15796  gausslemma2dlem1a  15806  gausslemma2dlem4  15812  gausslemma2dlem5a  15813  gausslemma2dlem5  15814  gausslemma2dlem6  15815  gausslemma2dlem7  15816  gausslemma2d  15817  lgseisenlem1  15818  lgseisenlem2  15819  lgseisenlem3  15820  lgseisenlem4  15821  lgseisen  15822  lgsquadlem1  15825  lgsquadlem2  15826  lgsquad2lem1  15829  lgsquad2lem2  15830  lgsquad3  15832  m1lgs  15833  2lgslem1a  15836  2lgslem1c  15838  2lgslem3a  15841  2lgslem3b  15842  2lgslem3c  15843  2lgslem3d  15844  2lgslem3a1  15845  2lgslem3b1  15846  2lgslem3c1  15847  2lgslem3d1  15848  2lgsoddprmlem1  15853  2lgsoddprmlem2  15854  2lgsoddprmlem3  15859  2sqlem1  15862  2sqlem2  15863  mul2sq  15864  2sqlem3  15865  2sqlem4  15866  2sqlem8  15871  2sqlem9  15872  2sqlem10  15873  vdegp1bid  16185  uspgr2wlkeqi  16237  isclwwlk  16264  clwwlkccatlem  16270  clwwlknonex2  16309  trilpolemeq1  16695  trilpolemlt1  16696  trirec0xor  16700  apdifflemf  16701  apdiff  16703  qdiff  16704  gsumgfsumlem  16735  gsumgfsum  16736