Theorem oveq1d 6073

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

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

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 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061

This theorem is referenced by:  fvoveq1d  6080  csbov2g  6100  caovassg  6221  caovdig  6237  caovdirg  6240  caov12d  6244  caov31d  6245  caov411d  6248  caofinvl  6301  suppofss1dcl  6477  suppofss2dcl  6478  omsuc  6718  nnmsucr  6734  nnm1  6771  nnm2  6772  ecovass  6891  ecoviass  6892  ecovdi  6893  ecovidi  6894  isacnm  7523  addasspig  7661  mulasspig  7663  mulpipq2  7702  distrnqg  7718  ltsonq  7729  ltanqg  7731  ltmnqg  7732  ltexnqq  7739  archnqq  7748  prarloclemarch2  7750  enq0sym  7763  addnq0mo  7778  mulnq0mo  7779  addnnnq0  7780  nqpnq0nq  7784  nq0m0r  7787  nq0a0  7788  nnanq0  7789  distrnq0  7790  addassnq0  7793  addpinq1  7795  prarloclemlo  7825  prarloclem3  7828  prarloclem5  7831  prarloclemcalc  7833  addnqprllem  7858  addnqprulem  7859  appdivnq  7894  recexprlem1ssl  7964  recexprlem1ssu  7965  ltmprr  7973  cauappcvgprlemladdru  7987  cauappcvgprlem1  7990  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemcl  8007  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprlem1  8010  caucvgprprlemcbv  8018  caucvgprprlemval  8019  caucvgprprlemexb  8038  caucvgprprlem1  8040  addcmpblnr  8070  mulcmpblnrlemg  8071  addsrmo  8074  mulsrmo  8075  addsrpr  8076  mulsrpr  8077  ltsrprg  8078  1idsr  8099  pn0sr  8102  recexgt0sr  8104  mulgt0sr  8109  srpospr  8114  prsradd  8117  caucvgsrlemfv  8122  caucvgsrlemcau  8124  caucvgsrlemgt1  8126  caucvgsrlemoffval  8127  caucvgsrlemoffcau  8129  caucvgsrlemoffres  8131  caucvgsrlembnd  8132  caucvgsr  8133  map2psrprg  8136  pitonnlem1p1  8177  pitonnlem2  8178  pitonn  8179  recidpirqlemcalc  8188  ax1rid  8208  axrnegex  8210  axcnre  8212  recriota  8221  nntopi  8225  axcaucvglemval  8228  axcaucvglemcau  8229  axcaucvglemres  8230  mul12  8418  mul4  8421  muladd11  8422  readdcan  8429  muladd11r  8445  add12  8447  cnegex  8467  addcan  8469  negeu  8480  pncan2  8496  addsubass  8499  addsub  8500  2addsub  8503  addsubeq4  8504  subid  8508  subid1  8509  npncan  8510  nppcan  8511  nnpcan  8512  nnncan1  8525  npncan3  8527  pnpcan  8528  pnncan  8530  ppncan  8531  addsub4  8532  negsub  8537  subneg  8538  subeqxfrd  8652  mvlraddd  8653  mvlladdd  8654  mvrraddd  8655  subaddeqd  8658  ine0  8684  mulneg1  8685  ltadd2  8710  apreap  8878  cru  8893  recexap  8944  mulcanapd  8952  div23ap  8982  div13ap  8984  divmulassap  8986  divmulasscomap  8987  divcanap4  8990  muldivdirap  8998  divsubdirap  8999  divmuldivap  9003  divdivdivap  9004  divcanap5  9005  divmul13ap  9006  divmuleqap  9008  divdiv32ap  9011  divcanap7  9012  dmdcanap  9013  divdivap1  9014  divdivap2  9015  divadddivap  9018  divsubdivap  9019  conjmulap  9020  divneg2ap  9027  subrecap  9130  mvllmulapd  9133  lt2mul2div  9170  nndivtr  9296  2halves  9484  halfaddsub  9489  subhalfhalf  9490  avgle1  9496  avgle2  9497  div4p1lem1div2  9509  un0addcl  9546  un0mulcl  9547  peano2z  9630  zneo  9697  nneoor  9698  nneo  9699  zeo  9701  zeo2  9702  deceq1  9731  qreccl  9992  xaddcom  10213  xnegdi  10220  xaddass  10221  xaddass2  10222  xpncan  10223  xleadd1a  10225  xltadd1  10228  xposdif  10234  xadd4d  10237  lincmb01cmp  10355  lincmble  10356  iccf1o  10357  fzspl  10425  fz0to4untppr  10480  fzo0addel  10555  fzosubel3  10563  qavgle  10642  2tnp1ge0ge0  10685  fldiv4p1lem1div2  10689  fldiv4lem1div2  10691  ceilqm1lt  10698  flqdiv  10707  modqlt  10719  modqdiffl  10721  modqcyc2  10746  modqaddabs  10748  mulqaddmodid  10750  mulp1mod1  10751  modqmuladd  10752  modqmuladdnn0  10754  qnegmod  10755  addmodid  10758  addmodidr  10759  modqadd2mod  10760  modqm1p1mod0  10761  modqmul12d  10764  modqnegd  10765  modqadd12d  10766  modqsub12d  10767  q2submod  10771  modqmulmodr  10776  modqaddmulmod  10777  modqsubdir  10779  modfzo0difsn  10781  modsumfzodifsn  10782  addmodlteq  10784  frecuzrdgsuc  10800  frecfzennn  10812  iseqovex  10844  seq3-1p  10876  seq3caopr2  10879  seqcaopr2g  10880  seq3caopr  10881  seqcaoprg  10882  seqf1oglem2a  10904  seqf1oglem1  10905  seqf1oglem2  10906  seq3id  10911  seq3homo  10913  seq3z  10914  seqhomog  10916  seqfeq4g  10917  expp1  10932  exprecap  10966  expaddzaplem  10968  expmulzap  10971  expdivap  10976  sqval  10983  sqsubswap  10985  sqdividap  10990  subsq  11032  subsq2  11033  binom2  11037  binom2sub  11039  mulbinom2  11042  binom3  11043  zesq  11045  bernneq2  11048  modqexp  11053  sqoddm1div8  11080  mulsubdivbinom2ap  11098  nn0opthlem1d  11107  nn0opthd  11109  nn0opth2d  11110  facp1  11117  facdiv  11125  facndiv  11126  faclbnd  11128  faclbnd2  11129  faclbnd3  11130  bcval  11136  bccmpl  11141  bcm1k  11147  bcp1n  11148  bcp1nk  11149  bcval5  11150  bcp1m1  11152  bcpasc  11153  bcm1n  11156  bcn2m1  11157  hashprg  11198  hashdifpr  11210  hashfzo  11212  hashfzp1  11214  hashfz0  11215  hashxp  11216  hashfibclem  11231  hashfibc  11232  zfz1isolemsplit  11235  zfz1isolem1  11237  seq3coll  11239  lswwrd  11296  ccatfvalfi  11305  ccatass  11321  lswccatn0lsw  11324  wrdlenccats1lenm1g  11349  ccatw2s1leng  11351  ccatswrd  11387  ccatpfx  11418  swrdpfx  11424  pfxpfx  11425  ccats1pfxeq  11431  wrdeqs1cat  11437  wrdind  11439  wrd2ind  11440  pfxccatpfx2  11454  pfxccatin12d  11462  cats1catd  11485  cats2catd  11486  s2leng  11506  s3s4d  11520  s2s5d  11521  s5s2d  11522  reval  11559  crre  11567  remim  11570  remul2  11583  immul2  11590  imval2  11604  cjdivap  11619  caucvgre  11691  cvg1nlemcau  11694  cvg1nlemres  11695  resqrexlemp1rp  11716  resqrexlemfp1  11719  resqrexlemover  11720  resqrexlemcalc1  11724  resqrexlemcalc3  11726  resqrexlemnm  11728  resqrexlemoverl  11731  resqrexlemglsq  11732  resqrexlemga  11733  resqrexlemsqa  11734  resqrexlemex  11735  resqrex  11736  sqrtdiv  11752  absvalsq  11763  absreimsq  11777  absdivap  11780  cau3lem  11824  maxabslemlub  11917  maxabslemval  11918  max0addsup  11929  minabs  11946  bdtrilem  11949  bdtri  11950  xrmaxaddlem  11970  xrmaxadd  11971  xrbdtri  11986  clim  11991  clim2  11993  climshftlemg  12012  climshft2  12016  climcn1  12018  climcn2  12019  subcn2  12021  reccn2ap  12023  climmulc2  12041  climsubc2  12043  clim2ser  12047  iser3shft  12056  climcau  12057  serf0  12062  fzosump1  12128  fsum1p  12129  fsump1  12131  sumsplitdc  12143  fsump1i  12144  mptfzshft  12153  fisum0diag2  12158  fsumconst  12165  fsumdifsnconst  12166  modfsummodlemstep  12168  modfsummod  12169  telfsumo  12177  fsumparts  12181  fsumrelem  12182  hash2iun1dif1  12191  binomlem  12194  binom  12195  binom1p  12196  binom1dif  12198  bcxmas  12200  isumsplit  12202  isum1p  12203  arisum  12209  arisum2  12210  trireciplem  12211  geoserap  12218  geolim  12222  geolim2  12223  georeclim  12224  geo2sum  12225  geoisum1  12230  cvgratnnlemseq  12237  cvgratnnlemsumlt  12239  cvgratnnlemfm  12240  cvgratz  12243  mertenslemi1  12246  mertenslem2  12247  mertensabs  12248  fprod1p  12310  fprodp1  12311  fprodcl2lem  12316  fprodfac  12326  fprodeq0  12328  fprodconst  12331  fprodrec  12340  fprodsplit1f  12345  fprodmodd  12352  efcllemp  12369  ef0lem  12371  efval  12372  esum  12373  ege2le3  12382  efaddlem  12385  efsep  12402  effsumlt  12403  eft0val  12404  efgt1p2  12406  efgt1p  12407  sinval  12413  cosval  12414  resinval  12426  recosval  12427  efi4p  12428  resin4p  12429  recos4p  12430  sinneg  12437  cosneg  12438  efival  12443  sinadd  12447  cosadd  12448  tanaddap  12450  sinmul  12455  cosmul  12456  cos2t  12461  cos2tsin  12462  ef01bndlem  12467  absefib  12482  demoivre  12484  demoivreALT  12485  eirraplem  12488  p1modz1  12505  dvdsmodexp  12506  moddvds  12510  mulmoddvds  12574  3dvds2dec  12577  zeo3  12579  odd2np1lem  12583  odd2np1  12584  oexpneg  12588  2tp1odd  12595  ltoddhalfle  12604  opoe  12606  opeo  12608  omeo  12609  m1expo  12611  m1exp1  12612  nn0o1gt2  12616  nn0o  12618  divalglemnn  12629  divalglemqt  12630  divalglemeunn  12632  divalglemex  12633  divalglemeuneg  12634  flodddiv4  12647  flodddiv4t2lthalf  12650  bitsp1o  12664  bitsmod  12667  bitsinv1lem  12672  gcdaddm  12705  bezoutlemnewy  12717  bezoutlema  12720  bezoutlemb  12721  bezoutlemex  12722  bezoutlemaz  12724  mulgcd  12737  gcddiv  12740  gcdmultiplez  12742  rpmulgcd  12747  rplpwr  12748  uzwodc  12758  lcmgcdlem  12799  lcmgcd  12800  divgcdcoprmex  12824  cncongr2  12826  prmexpb  12873  rpexp  12875  rpexp1i  12876  sqrt2irrlem  12883  oddpwdclemxy  12891  oddpwdclemndvds  12893  sqpweven  12897  2sqpwodd  12898  sqne2sq  12899  qmuldeneqnum  12917  nn0gcdsq  12922  zgcdsq  12923  numdensq  12924  dfphi2  12942  phiprmpw  12944  phiprm  12945  eulerthlema  12952  eulerthlemh  12953  eulerthlemth  12954  fermltl  12956  prmdiv  12957  prmdiveq  12958  prmdivdiv  12959  hashgcdlem  12960  odzval  12964  odzcllem  12965  odzdvds  12968  vfermltl  12974  powm2modprm  12975  reumodprminv  12976  modprm0  12977  nnnn0modprm0  12978  modprmn0modprm0  12979  coprimeprodsq  12980  coprimeprodsq2  12981  pythagtriplem1  12988  pythagtriplem3  12990  pythagtriplem4  12991  pythagtriplem6  12993  pythagtriplem7  12994  pythagtriplem12  12998  pythagtriplem14  13000  pythagtriplem15  13001  pythagtriplem16  13002  pythagtriplem17  13003  pythagtriplem18  13004  pceu  13018  pczpre  13020  pcdiv  13025  pcqdiv  13030  pcrec  13031  pczndvds  13039  pcneg  13048  pc2dvds  13053  pcprmpw2  13056  pcaddlem  13062  pcadd  13063  fldivp1  13071  pockthlem  13079  pockthi  13081  4sqlem5  13105  4sqlem9  13109  4sqlem10  13110  4sqlem2  13112  4sqlem3  13113  4sqlem4  13115  mul4sqlem  13116  4sqlem11  13124  4sqlem12  13125  4sqlem14  13127  4sqlem15  13128  4sqlem17  13130  4sqlem19  13132  ballotfilem2  13172  ballotfilemfp1  13175  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilem4  13185  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemsval  13196  ballotfilemsdom  13199  ballotfilemsima  13203  ballotfilemieq  13204  ballotfilemfrci  13215  ballotfilemth  13225  ballotfi  13226  ennnfonelemkh  13247  ennnfonelemhf1o  13248  setscomd  13337  ressressg  13372  qusex  13589  qusin  13590  grpinvalem  13648  grpinva  13649  grprida  13650  gsumsplit1r  13661  isnsgrp  13669  sgrpass  13671  sgrp1  13674  sgrppropd  13676  mnd12g  13689  mndpropd  13701  imasmnd2  13707  mhmex  13717  mhmlin  13722  grprcan  13792  grpinvid1  13807  isgrpinv  13809  grplcan  13817  grpasscan1  13818  grplmulf1o  13829  grpinvadd  13833  grpinvsub  13837  grpsubsub4  13848  grppnpcan2  13849  grpnpncan  13850  dfgrp3mlem  13853  dfgrp3m  13854  grplactcnv  13857  imasgrp2  13863  mhmlem  13867  mhmid  13868  mhmmnd  13869  mulgnnp1  13883  mulg2  13884  mulgnn0p1  13886  mulgsubcl  13889  mulgneg  13893  mulgaddcomlem  13898  mulgaddcom  13899  mulgz  13903  mulgnn0dir  13905  mulgdirlem  13906  mulgdir  13907  mulgneg2  13909  mulgnnass  13910  mulgnn0ass  13911  mulgass  13912  mulgassr  13913  mulgmodid  13914  mulgsubdir  13915  submmulg  13919  isnsg3  13960  nmzsubg  13963  ssnmz  13964  0nsg  13967  eqger  13977  eqgid  13979  eqgcpbl  13981  ghmlin  14001  ghmmulg  14009  ghmnsgima  14021  ghmnsgpreima  14022  conjghm  14029  conjnmz  14032  ablsub2inv  14064  abladdsub4  14067  abladdsub  14068  ablpncan2  14069  ablpnpcan  14073  ablnncan  14074  ablnnncan1  14077  gsumfzconst  14094  gsumfzsnfd  14098  gsumsplit0  14099  gsumshift  14105  gsumgfsum  14106  prdssgrpd  14133  prdsidlem  14135  prdsmndd  14136  prdsinvlem  14138  mgpress  14170  rngass  14178  rngdi  14179  rngdir  14180  rnglz  14184  rngmneg1  14186  rngsubdir  14191  rngpropd  14194  imasrng  14195  srgass  14214  srgmulgass  14232  srgpcomp  14233  srgpcompp  14234  srgpcomppsc  14235  ringpropd  14281  ringlz  14286  ring1eq0  14291  ringnegl  14294  ringmneg1  14296  ringsubdir  14300  mulgass2  14301  ring1  14302  imasring  14307  opprrng  14320  opprring  14322  unitgrp  14361  dvrcan1  14385  rdivmuldivd  14389  subrginv  14483  resrhm  14494  unitrrg  14514  aprlring  14538  islmod  14565  lmodlema  14566  islmodd  14567  lmod0vs  14595  lmodvs0  14596  lmodvsmmulgdi  14597  lmodvneg1  14604  lmodvsneg  14605  lmodsubvs  14617  lmodsubdi  14618  lmodsubdir  14619  lmodprop2d  14622  rmodislmodlem  14624  rmodislmod  14625  lsssetm  14630  islssmd  14633  lssclg  14638  lssvacl  14639  lss1d  14657  lsspropdg  14705  sraval  14711  rnglidlmcl  14754  gsumfzfsumlemm  14861  znunit  14933  mplsubgfilemcl  14980  resttop  15161  restco  15165  restin  15167  lmfval  15184  cnprcl2k  15197  txrest  15267  txdis1cn  15269  cnmpt2res  15288  psmettri2  15319  psmettri  15321  xmettri2  15352  xmettri  15363  mettri  15364  metrtri  15368  blvalps  15379  blval  15380  xblss2  15396  blhalf  15399  comet  15490  xmetxp  15498  txmetcnp  15509  cnmet  15521  ioo2bl  15542  ivthreinc  15636  limcmpted  15654  limcimolemlt  15655  cnplimclemr  15660  limccnp2cntop  15668  reldvg  15670  dvfvalap  15672  dvidlemap  15682  dvidrelem  15683  dvidsslem  15684  dvconst  15685  dvconstre  15687  dvconstss  15689  dvcnp2cntop  15690  dvaddxxbr  15692  dvmulxxbr  15693  dvcoapbr  15698  dvcjbr  15699  dvexp  15702  dvrecap  15704  dvmptcmulcn  15712  dveflem  15717  plyval  15723  elply2  15726  elplyr  15731  elplyd  15732  ply1termlem  15733  plyaddlem1  15738  plymullem1  15739  plycoeid3  15748  plycjlemc  15751  dvply1  15756  sin0pilem1  15772  sinperlem  15799  ptolemy  15815  tangtx  15829  abssinper  15837  reexplog  15862  relogexp  15863  cxprec  15901  rpdivcxp  15902  cxpmul  15903  rpabscxpbnd  15931  rplogbval  15936  rplogbreexp  15944  rprelogbmul  15946  logbrec  15951  logbgcd1irraplemap  15960  binom4  15970  pellexlem2  15972  pellexlem3  15973  wilthlem1  15974  mpodvdsmulf1o  15984  sgmppw  15986  0sgmppw  15987  1sgmprm  15988  1sgm2ppw  15989  perfectlem1  15993  perfectlem2  15994  perfect  15995  lgslem1  15999  lgslem4  16002  lgsval  16003  lgsfvalg  16004  lgsval2lem  16009  lgsval4lem  16010  lgsvalmod  16018  lgsneg  16023  lgsneg1  16024  lgsmod  16025  lgsdilem  16026  lgsdir2lem4  16030  lgsdir2  16032  lgsdirprm  16033  lgsdir  16034  lgsne0  16037  lgssq  16039  lgssq2  16040  lgsmulsqcoprm  16045  lgsdirnn0  16046  lgsdinn0  16047  gausslemma2dlem1a  16057  gausslemma2dlem4  16063  gausslemma2dlem5a  16064  gausslemma2dlem5  16065  gausslemma2dlem6  16066  gausslemma2dlem7  16067  gausslemma2d  16068  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisenlem4  16072  lgseisen  16073  lgsquadlem1  16076  lgsquadlem2  16077  lgsquad2lem1  16080  lgsquad2lem2  16081  lgsquad3  16083  m1lgs  16084  2lgslem1a  16087  2lgslem1c  16089  2lgslem3a  16092  2lgslem3b  16093  2lgslem3c  16094  2lgslem3d  16095  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  2lgsoddprmlem1  16104  2lgsoddprmlem2  16105  2lgsoddprmlem3  16110  2sqlem1  16113  2sqlem2  16114  mul2sq  16115  2sqlem3  16116  2sqlem4  16117  2sqlem8  16122  2sqlem9  16123  2sqlem10  16124  vdegp1bid  16436  uspgr2wlkeqi  16488  isclwwlk  16515  clwwlkccatlem  16521  clwwlknonex2  16560  repiecele0  16936  repiecege0  16937  repiecef  16938  trilpolemeq1  16950  trilpolemlt1  16951  trirec0xor  16955  apdifflemf  16956  apdiff  16958  qdiff  16959