Theorem oveq1d 6032

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

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

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 6020

This theorem is referenced by:  fvoveq1d  6039  csbov2g  6059  caovassg  6180  caovdig  6196  caovdirg  6199  caov12d  6203  caov31d  6204  caov411d  6207  caofinvl  6260  omsuc  6639  nnmsucr  6655  nnm1  6692  nnm2  6693  ecovass  6812  ecoviass  6813  ecovdi  6814  ecovidi  6815  isacnm  7417  addasspig  7549  mulasspig  7551  mulpipq2  7590  distrnqg  7606  ltsonq  7617  ltanqg  7619  ltmnqg  7620  ltexnqq  7627  archnqq  7636  prarloclemarch2  7638  enq0sym  7651  addnq0mo  7666  mulnq0mo  7667  addnnnq0  7668  nqpnq0nq  7672  nq0m0r  7675  nq0a0  7676  nnanq0  7677  distrnq0  7678  addassnq0  7681  addpinq1  7683  prarloclemlo  7713  prarloclem3  7716  prarloclem5  7719  prarloclemcalc  7721  addnqprllem  7746  addnqprulem  7747  appdivnq  7782  recexprlem1ssl  7852  recexprlem1ssu  7853  ltmprr  7861  cauappcvgprlemladdru  7875  cauappcvgprlem1  7878  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemcl  7895  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprlem1  7898  caucvgprprlemcbv  7906  caucvgprprlemval  7907  caucvgprprlemexb  7926  caucvgprprlem1  7928  addcmpblnr  7958  mulcmpblnrlemg  7959  addsrmo  7962  mulsrmo  7963  addsrpr  7964  mulsrpr  7965  ltsrprg  7966  1idsr  7987  pn0sr  7990  recexgt0sr  7992  mulgt0sr  7997  srpospr  8002  prsradd  8005  caucvgsrlemfv  8010  caucvgsrlemcau  8012  caucvgsrlemgt1  8014  caucvgsrlemoffval  8015  caucvgsrlemoffcau  8017  caucvgsrlemoffres  8019  caucvgsrlembnd  8020  caucvgsr  8021  map2psrprg  8024  pitonnlem1p1  8065  pitonnlem2  8066  pitonn  8067  recidpirqlemcalc  8076  ax1rid  8096  axrnegex  8098  axcnre  8100  recriota  8109  nntopi  8113  axcaucvglemval  8116  axcaucvglemcau  8117  axcaucvglemres  8118  mul12  8307  mul4  8310  muladd11  8311  readdcan  8318  muladd11r  8334  add12  8336  cnegex  8356  addcan  8358  negeu  8369  pncan2  8385  addsubass  8388  addsub  8389  2addsub  8392  addsubeq4  8393  subid  8397  subid1  8398  npncan  8399  nppcan  8400  nnpcan  8401  nnncan1  8414  npncan3  8416  pnpcan  8417  pnncan  8419  ppncan  8420  addsub4  8421  negsub  8426  subneg  8427  subeqxfrd  8541  mvlraddd  8542  mvlladdd  8543  mvrraddd  8544  subaddeqd  8547  ine0  8572  mulneg1  8573  ltadd2  8598  apreap  8766  cru  8781  recexap  8832  mulcanapd  8840  div23ap  8870  div13ap  8872  divmulassap  8874  divmulasscomap  8875  divcanap4  8878  muldivdirap  8886  divsubdirap  8887  divmuldivap  8891  divdivdivap  8892  divcanap5  8893  divmul13ap  8894  divmuleqap  8896  divdiv32ap  8899  divcanap7  8900  dmdcanap  8901  divdivap1  8902  divdivap2  8903  divadddivap  8906  divsubdivap  8907  conjmulap  8908  divneg2ap  8915  subrecap  9018  mvllmulapd  9021  lt2mul2div  9058  nndivtr  9184  2halves  9372  halfaddsub  9377  subhalfhalf  9378  avgle1  9384  avgle2  9385  div4p1lem1div2  9397  un0addcl  9434  un0mulcl  9435  peano2z  9514  zneo  9580  nneoor  9581  nneo  9582  zeo  9584  zeo2  9585  deceq1  9614  qreccl  9875  xaddcom  10095  xnegdi  10102  xaddass  10103  xaddass2  10104  xpncan  10105  xleadd1a  10107  xltadd1  10110  xposdif  10116  xadd4d  10119  lincmb01cmp  10237  iccf1o  10238  fz0to4untppr  10358  fzo0addel  10432  fzosubel3  10440  qavgle  10517  2tnp1ge0ge0  10560  fldiv4p1lem1div2  10564  fldiv4lem1div2  10566  ceilqm1lt  10573  flqdiv  10582  modqlt  10594  modqdiffl  10596  modqcyc2  10621  modqaddabs  10623  mulqaddmodid  10625  mulp1mod1  10626  modqmuladd  10627  modqmuladdnn0  10629  qnegmod  10630  addmodid  10633  addmodidr  10634  modqadd2mod  10635  modqm1p1mod0  10636  modqmul12d  10639  modqnegd  10640  modqadd12d  10641  modqsub12d  10642  q2submod  10646  modqmulmodr  10651  modqaddmulmod  10652  modqsubdir  10654  modfzo0difsn  10656  modsumfzodifsn  10657  addmodlteq  10659  frecuzrdgsuc  10675  frecfzennn  10687  iseqovex  10719  seq3-1p  10751  seq3caopr2  10754  seqcaopr2g  10755  seq3caopr  10756  seqcaoprg  10757  seqf1oglem2a  10779  seqf1oglem1  10780  seqf1oglem2  10781  seq3id  10786  seq3homo  10788  seq3z  10789  seqhomog  10791  seqfeq4g  10792  expp1  10807  exprecap  10841  expaddzaplem  10843  expmulzap  10846  expdivap  10851  sqval  10858  sqsubswap  10860  sqdividap  10865  subsq  10907  subsq2  10908  binom2  10912  binom2sub  10914  mulbinom2  10917  binom3  10918  zesq  10919  bernneq2  10922  modqexp  10927  sqoddm1div8  10954  mulsubdivbinom2ap  10972  nn0opthlem1d  10981  nn0opthd  10983  nn0opth2d  10984  facp1  10991  facdiv  10999  facndiv  11000  faclbnd  11002  faclbnd2  11003  faclbnd3  11004  bcval  11010  bccmpl  11015  bcm1k  11021  bcp1n  11022  bcp1nk  11023  bcval5  11024  bcp1m1  11026  bcpasc  11027  bcn2m1  11030  hashprg  11071  hashdifpr  11083  hashfzo  11085  hashfzp1  11087  hashfz0  11088  hashxp  11089  zfz1isolemsplit  11101  zfz1isolem1  11103  seq3coll  11105  lswwrd  11159  ccatfvalfi  11168  ccatass  11184  lswccatn0lsw  11187  wrdlenccats1lenm1g  11212  ccatw2s1leng  11214  ccatswrd  11250  ccatpfx  11281  swrdpfx  11287  pfxpfx  11288  ccats1pfxeq  11294  wrdeqs1cat  11300  wrdind  11302  wrd2ind  11303  pfxccatpfx2  11317  pfxccatin12d  11325  cats1catd  11348  cats2catd  11349  s2leng  11369  reval  11409  crre  11417  remim  11420  remul2  11433  immul2  11440  imval2  11454  cjdivap  11469  caucvgre  11541  cvg1nlemcau  11544  cvg1nlemres  11545  resqrexlemp1rp  11566  resqrexlemfp1  11569  resqrexlemover  11570  resqrexlemcalc1  11574  resqrexlemcalc3  11576  resqrexlemnm  11578  resqrexlemoverl  11581  resqrexlemglsq  11582  resqrexlemga  11583  resqrexlemsqa  11584  resqrexlemex  11585  resqrex  11586  sqrtdiv  11602  absvalsq  11613  absreimsq  11627  absdivap  11630  cau3lem  11674  maxabslemlub  11767  maxabslemval  11768  max0addsup  11779  minabs  11796  bdtrilem  11799  bdtri  11800  xrmaxaddlem  11820  xrmaxadd  11821  xrbdtri  11836  clim  11841  clim2  11843  climshftlemg  11862  climshft2  11866  climcn1  11868  climcn2  11869  subcn2  11871  reccn2ap  11873  climmulc2  11891  climsubc2  11893  clim2ser  11897  iser3shft  11906  climcau  11907  serf0  11912  fzosump1  11977  fsum1p  11978  fsump1  11980  sumsplitdc  11992  fsump1i  11993  mptfzshft  12002  fisum0diag2  12007  fsumconst  12014  fsumdifsnconst  12015  modfsummodlemstep  12017  modfsummod  12018  telfsumo  12026  fsumparts  12030  fsumrelem  12031  hash2iun1dif1  12040  binomlem  12043  binom  12044  binom1p  12045  binom1dif  12047  bcxmas  12049  isumsplit  12051  isum1p  12052  arisum  12058  arisum2  12059  trireciplem  12060  geoserap  12067  geolim  12071  geolim2  12072  georeclim  12073  geo2sum  12074  geoisum1  12079  cvgratnnlemseq  12086  cvgratnnlemsumlt  12088  cvgratnnlemfm  12089  cvgratz  12092  mertenslemi1  12095  mertenslem2  12096  mertensabs  12097  fprod1p  12159  fprodp1  12160  fprodcl2lem  12165  fprodfac  12175  fprodeq0  12177  fprodconst  12180  fprodrec  12189  fprodsplit1f  12194  fprodmodd  12201  efcllemp  12218  ef0lem  12220  efval  12221  esum  12222  ege2le3  12231  efaddlem  12234  efsep  12251  effsumlt  12252  eft0val  12253  efgt1p2  12255  efgt1p  12256  sinval  12262  cosval  12263  resinval  12275  recosval  12276  efi4p  12277  resin4p  12278  recos4p  12279  sinneg  12286  cosneg  12287  efival  12292  sinadd  12296  cosadd  12297  tanaddap  12299  sinmul  12304  cosmul  12305  cos2t  12310  cos2tsin  12311  ef01bndlem  12316  absefib  12331  demoivre  12333  demoivreALT  12334  eirraplem  12337  p1modz1  12354  dvdsmodexp  12355  moddvds  12359  mulmoddvds  12423  3dvds2dec  12426  zeo3  12428  odd2np1lem  12432  odd2np1  12433  oexpneg  12437  2tp1odd  12444  ltoddhalfle  12453  opoe  12455  opeo  12457  omeo  12458  m1expo  12460  m1exp1  12461  nn0o1gt2  12465  nn0o  12467  divalglemnn  12478  divalglemqt  12479  divalglemeunn  12481  divalglemex  12482  divalglemeuneg  12483  flodddiv4  12496  flodddiv4t2lthalf  12499  bitsp1o  12513  bitsmod  12516  bitsinv1lem  12521  gcdaddm  12554  bezoutlemnewy  12566  bezoutlema  12569  bezoutlemb  12570  bezoutlemex  12571  bezoutlemaz  12573  mulgcd  12586  gcddiv  12589  gcdmultiplez  12591  rpmulgcd  12596  rplpwr  12597  uzwodc  12607  lcmgcdlem  12648  lcmgcd  12649  divgcdcoprmex  12673  cncongr2  12675  prmexpb  12722  rpexp  12724  rpexp1i  12725  sqrt2irrlem  12732  oddpwdclemxy  12740  oddpwdclemndvds  12742  sqpweven  12746  2sqpwodd  12747  sqne2sq  12748  qmuldeneqnum  12766  nn0gcdsq  12771  zgcdsq  12772  numdensq  12773  dfphi2  12791  phiprmpw  12793  phiprm  12794  eulerthlema  12801  eulerthlemh  12802  eulerthlemth  12803  fermltl  12805  prmdiv  12806  prmdiveq  12807  prmdivdiv  12808  hashgcdlem  12809  odzval  12813  odzcllem  12814  odzdvds  12817  vfermltl  12823  powm2modprm  12824  reumodprminv  12825  modprm0  12826  nnnn0modprm0  12827  modprmn0modprm0  12828  coprimeprodsq  12829  coprimeprodsq2  12830  pythagtriplem1  12837  pythagtriplem3  12839  pythagtriplem4  12840  pythagtriplem6  12842  pythagtriplem7  12843  pythagtriplem12  12847  pythagtriplem14  12849  pythagtriplem15  12850  pythagtriplem16  12851  pythagtriplem17  12852  pythagtriplem18  12853  pceu  12867  pczpre  12869  pcdiv  12874  pcqdiv  12879  pcrec  12880  pczndvds  12888  pcneg  12897  pc2dvds  12902  pcprmpw2  12905  pcaddlem  12911  pcadd  12912  fldivp1  12920  pockthlem  12928  pockthi  12930  4sqlem5  12954  4sqlem9  12958  4sqlem10  12959  4sqlem2  12961  4sqlem3  12962  4sqlem4  12964  mul4sqlem  12965  4sqlem11  12973  4sqlem12  12974  4sqlem14  12976  4sqlem15  12977  4sqlem17  12979  4sqlem19  12981  ennnfonelemkh  13032  ennnfonelemhf1o  13033  setscomd  13122  ressressg  13157  qusex  13407  qusin  13408  grpinvalem  13467  grpinva  13468  grprida  13469  gsumsplit1r  13480  isnsgrp  13488  sgrpass  13490  sgrp1  13493  sgrppropd  13495  prdssgrpd  13497  mnd12g  13510  mndpropd  13522  prdsidlem  13529  prdsmndd  13530  imasmnd2  13534  mhmex  13544  mhmlin  13549  grprcan  13619  grpinvid1  13634  isgrpinv  13636  grplcan  13644  grpasscan1  13645  grplmulf1o  13656  grpinvadd  13660  grpinvsub  13664  grpsubsub4  13675  grppnpcan2  13676  grpnpncan  13677  dfgrp3mlem  13680  dfgrp3m  13681  grplactcnv  13684  prdsinvlem  13690  imasgrp2  13696  mhmlem  13700  mhmid  13701  mhmmnd  13702  mulgnnp1  13716  mulg2  13717  mulgnn0p1  13719  mulgsubcl  13722  mulgneg  13726  mulgaddcomlem  13731  mulgaddcom  13732  mulgz  13736  mulgnn0dir  13738  mulgdirlem  13739  mulgdir  13740  mulgneg2  13742  mulgnnass  13743  mulgnn0ass  13744  mulgass  13745  mulgassr  13746  mulgmodid  13747  mulgsubdir  13748  submmulg  13752  isnsg3  13793  nmzsubg  13796  ssnmz  13797  0nsg  13800  eqger  13810  eqgid  13812  eqgcpbl  13814  ghmlin  13834  ghmmulg  13842  ghmnsgima  13854  ghmnsgpreima  13855  conjghm  13862  conjnmz  13865  ablsub2inv  13897  abladdsub4  13900  abladdsub  13901  ablpncan2  13902  ablpnpcan  13906  ablnncan  13907  ablnnncan1  13910  gsumfzconst  13927  gsumfzsnfd  13931  mgpress  13943  rngass  13951  rngdi  13952  rngdir  13953  rnglz  13957  rngmneg1  13959  rngsubdir  13964  rngpropd  13967  imasrng  13968  srgass  13983  srgmulgass  14001  srgpcomp  14002  srgpcompp  14003  srgpcomppsc  14004  ringpropd  14050  ringlz  14055  ring1eq0  14060  ringnegl  14063  ringmneg1  14065  ringsubdir  14069  mulgass2  14070  ring1  14071  imasring  14076  opprrng  14089  opprring  14091  unitgrp  14129  dvrcan1  14153  rdivmuldivd  14157  subrginv  14250  resrhm  14261  unitrrg  14280  islmod  14304  lmodlema  14305  islmodd  14306  lmod0vs  14334  lmodvs0  14335  lmodvsmmulgdi  14336  lmodvneg1  14343  lmodvsneg  14344  lmodsubvs  14356  lmodsubdi  14357  lmodsubdir  14358  lmodprop2d  14361  rmodislmodlem  14363  rmodislmod  14364  lsssetm  14369  islssmd  14372  lssclg  14377  lssvacl  14378  lss1d  14396  lsspropdg  14444  sraval  14450  rnglidlmcl  14493  gsumfzfsumlemm  14600  znunit  14672  mplsubgfilemcl  14712  resttop  14893  restco  14897  restin  14899  lmfval  14916  cnprcl2k  14929  txrest  14999  txdis1cn  15001  cnmpt2res  15020  psmettri2  15051  psmettri  15053  xmettri2  15084  xmettri  15095  mettri  15096  metrtri  15100  blvalps  15111  blval  15112  xblss2  15128  blhalf  15131  comet  15222  xmetxp  15230  txmetcnp  15241  cnmet  15253  ioo2bl  15274  ivthreinc  15368  limcmpted  15386  limcimolemlt  15387  cnplimclemr  15392  limccnp2cntop  15400  reldvg  15402  dvfvalap  15404  dvidlemap  15414  dvidrelem  15415  dvidsslem  15416  dvconst  15417  dvconstre  15419  dvconstss  15421  dvcnp2cntop  15422  dvaddxxbr  15424  dvmulxxbr  15425  dvcoapbr  15430  dvcjbr  15431  dvexp  15434  dvrecap  15436  dvmptcmulcn  15444  dveflem  15449  plyval  15455  elply2  15458  elplyr  15463  elplyd  15464  ply1termlem  15465  plyaddlem1  15470  plymullem1  15471  plycoeid3  15480  plycjlemc  15483  dvply1  15488  sin0pilem1  15504  sinperlem  15531  ptolemy  15547  tangtx  15561  abssinper  15569  reexplog  15594  relogexp  15595  cxprec  15633  rpdivcxp  15634  cxpmul  15635  rpabscxpbnd  15663  rplogbval  15668  rplogbreexp  15676  rprelogbmul  15678  logbrec  15683  logbgcd1irraplemap  15692  binom4  15702  wilthlem1  15703  mpodvdsmulf1o  15713  sgmppw  15715  0sgmppw  15716  1sgmprm  15717  1sgm2ppw  15718  perfectlem1  15722  perfectlem2  15723  perfect  15724  lgslem1  15728  lgslem4  15731  lgsval  15732  lgsfvalg  15733  lgsval2lem  15738  lgsval4lem  15739  lgsvalmod  15747  lgsneg  15752  lgsneg1  15753  lgsmod  15754  lgsdilem  15755  lgsdir2lem4  15759  lgsdir2  15761  lgsdirprm  15762  lgsdir  15763  lgsne0  15766  lgssq  15768  lgssq2  15769  lgsmulsqcoprm  15774  lgsdirnn0  15775  lgsdinn0  15776  gausslemma2dlem1a  15786  gausslemma2dlem4  15792  gausslemma2dlem5a  15793  gausslemma2dlem5  15794  gausslemma2dlem6  15795  gausslemma2dlem7  15796  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisenlem4  15801  lgseisen  15802  lgsquadlem1  15805  lgsquadlem2  15806  lgsquad2lem1  15809  lgsquad2lem2  15810  lgsquad3  15812  m1lgs  15813  2lgslem1a  15816  2lgslem1c  15818  2lgslem3a  15821  2lgslem3b  15822  2lgslem3c  15823  2lgslem3d  15824  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  2lgsoddprmlem1  15833  2lgsoddprmlem2  15834  2lgsoddprmlem3  15839  2sqlem1  15842  2sqlem2  15843  mul2sq  15844  2sqlem3  15845  2sqlem4  15846  2sqlem8  15851  2sqlem9  15852  2sqlem10  15853  vdegp1bid  16165  uspgr2wlkeqi  16217  isclwwlk  16244  clwwlkccatlem  16250  clwwlknonex2  16289  trilpolemeq1  16644  trilpolemlt1  16645  trirec0xor  16649  apdifflemf  16650  apdiff  16652  gsumgfsumlem  16683  gsumgfsum  16684