Theorem oveq1d 5982

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

Syntax hints:   → wi 4   = wceq 1373  (class class class)co 5967

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 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-nfc 2339  df-rex 2492  df-v 2778  df-un 3178  df-sn 3649  df-pr 3650  df-op 3652  df-uni 3865  df-br 4060  df-iota 5251  df-fv 5298  df-ov 5970

This theorem is referenced by:  fvoveq1d  5989  csbov2g  6009  caovassg  6128  caovdig  6144  caovdirg  6147  caov12d  6151  caov31d  6152  caov411d  6155  caofinvl  6207  omsuc  6581  nnmsucr  6597  nnm1  6634  nnm2  6635  ecovass  6754  ecoviass  6755  ecovdi  6756  ecovidi  6757  isacnm  7346  addasspig  7478  mulasspig  7480  mulpipq2  7519  distrnqg  7535  ltsonq  7546  ltanqg  7548  ltmnqg  7549  ltexnqq  7556  archnqq  7565  prarloclemarch2  7567  enq0sym  7580  addnq0mo  7595  mulnq0mo  7596  addnnnq0  7597  nqpnq0nq  7601  nq0m0r  7604  nq0a0  7605  nnanq0  7606  distrnq0  7607  addassnq0  7610  addpinq1  7612  prarloclemlo  7642  prarloclem3  7645  prarloclem5  7648  prarloclemcalc  7650  addnqprllem  7675  addnqprulem  7676  appdivnq  7711  recexprlem1ssl  7781  recexprlem1ssu  7782  ltmprr  7790  cauappcvgprlemladdru  7804  cauappcvgprlem1  7807  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemcl  7824  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprlem1  7827  caucvgprprlemcbv  7835  caucvgprprlemval  7836  caucvgprprlemexb  7855  caucvgprprlem1  7857  addcmpblnr  7887  mulcmpblnrlemg  7888  addsrmo  7891  mulsrmo  7892  addsrpr  7893  mulsrpr  7894  ltsrprg  7895  1idsr  7916  pn0sr  7919  recexgt0sr  7921  mulgt0sr  7926  srpospr  7931  prsradd  7934  caucvgsrlemfv  7939  caucvgsrlemcau  7941  caucvgsrlemgt1  7943  caucvgsrlemoffval  7944  caucvgsrlemoffcau  7946  caucvgsrlemoffres  7948  caucvgsrlembnd  7949  caucvgsr  7950  map2psrprg  7953  pitonnlem1p1  7994  pitonnlem2  7995  pitonn  7996  recidpirqlemcalc  8005  ax1rid  8025  axrnegex  8027  axcnre  8029  recriota  8038  nntopi  8042  axcaucvglemval  8045  axcaucvglemcau  8046  axcaucvglemres  8047  mul12  8236  mul4  8239  muladd11  8240  readdcan  8247  muladd11r  8263  add12  8265  cnegex  8285  addcan  8287  negeu  8298  pncan2  8314  addsubass  8317  addsub  8318  2addsub  8321  addsubeq4  8322  subid  8326  subid1  8327  npncan  8328  nppcan  8329  nnpcan  8330  nnncan1  8343  npncan3  8345  pnpcan  8346  pnncan  8348  ppncan  8349  addsub4  8350  negsub  8355  subneg  8356  subeqxfrd  8470  mvlraddd  8471  mvlladdd  8472  mvrraddd  8473  subaddeqd  8476  ine0  8501  mulneg1  8502  ltadd2  8527  apreap  8695  cru  8710  recexap  8761  mulcanapd  8769  div23ap  8799  div13ap  8801  divmulassap  8803  divmulasscomap  8804  divcanap4  8807  muldivdirap  8815  divsubdirap  8816  divmuldivap  8820  divdivdivap  8821  divcanap5  8822  divmul13ap  8823  divmuleqap  8825  divdiv32ap  8828  divcanap7  8829  dmdcanap  8830  divdivap1  8831  divdivap2  8832  divadddivap  8835  divsubdivap  8836  conjmulap  8837  divneg2ap  8844  subrecap  8947  mvllmulapd  8950  lt2mul2div  8987  nndivtr  9113  2halves  9301  halfaddsub  9306  subhalfhalf  9307  avgle1  9313  avgle2  9314  div4p1lem1div2  9326  un0addcl  9363  un0mulcl  9364  peano2z  9443  zneo  9509  nneoor  9510  nneo  9511  zeo  9513  zeo2  9514  deceq1  9543  qreccl  9798  xaddcom  10018  xnegdi  10025  xaddass  10026  xaddass2  10027  xpncan  10028  xleadd1a  10030  xltadd1  10033  xposdif  10039  xadd4d  10042  lincmb01cmp  10160  iccf1o  10161  fz0to4untppr  10281  fzo0addel  10354  fzosubel3  10362  qavgle  10438  2tnp1ge0ge0  10481  fldiv4p1lem1div2  10485  fldiv4lem1div2  10487  ceilqm1lt  10494  flqdiv  10503  modqlt  10515  modqdiffl  10517  modqcyc2  10542  modqaddabs  10544  mulqaddmodid  10546  mulp1mod1  10547  modqmuladd  10548  modqmuladdnn0  10550  qnegmod  10551  addmodid  10554  addmodidr  10555  modqadd2mod  10556  modqm1p1mod0  10557  modqmul12d  10560  modqnegd  10561  modqadd12d  10562  modqsub12d  10563  q2submod  10567  modqmulmodr  10572  modqaddmulmod  10573  modqsubdir  10575  modfzo0difsn  10577  modsumfzodifsn  10578  addmodlteq  10580  frecuzrdgsuc  10596  frecfzennn  10608  iseqovex  10640  seq3-1p  10672  seq3caopr2  10675  seqcaopr2g  10676  seq3caopr  10677  seqcaoprg  10678  seqf1oglem2a  10700  seqf1oglem1  10701  seqf1oglem2  10702  seq3id  10707  seq3homo  10709  seq3z  10710  seqhomog  10712  seqfeq4g  10713  expp1  10728  exprecap  10762  expaddzaplem  10764  expmulzap  10767  expdivap  10772  sqval  10779  sqsubswap  10781  sqdividap  10786  subsq  10828  subsq2  10829  binom2  10833  binom2sub  10835  mulbinom2  10838  binom3  10839  zesq  10840  bernneq2  10843  modqexp  10848  sqoddm1div8  10875  mulsubdivbinom2ap  10893  nn0opthlem1d  10902  nn0opthd  10904  nn0opth2d  10905  facp1  10912  facdiv  10920  facndiv  10921  faclbnd  10923  faclbnd2  10924  faclbnd3  10925  bcval  10931  bccmpl  10936  bcm1k  10942  bcp1n  10943  bcp1nk  10944  bcval5  10945  bcp1m1  10947  bcpasc  10948  bcn2m1  10951  hashprg  10990  hashdifpr  11002  hashfzo  11004  hashfzp1  11006  hashfz0  11007  hashxp  11008  zfz1isolemsplit  11020  zfz1isolem1  11022  seq3coll  11024  lswwrd  11077  ccatfvalfi  11086  ccatass  11102  lswccatn0lsw  11105  ccatswrd  11161  ccatpfx  11192  swrdpfx  11198  pfxpfx  11199  ccats1pfxeq  11205  wrdeqs1cat  11211  wrdind  11213  wrd2ind  11214  pfxccatpfx2  11228  pfxccatin12d  11236  reval  11275  crre  11283  remim  11286  remul2  11299  immul2  11306  imval2  11320  cjdivap  11335  caucvgre  11407  cvg1nlemcau  11410  cvg1nlemres  11411  resqrexlemp1rp  11432  resqrexlemfp1  11435  resqrexlemover  11436  resqrexlemcalc1  11440  resqrexlemcalc3  11442  resqrexlemnm  11444  resqrexlemoverl  11447  resqrexlemglsq  11448  resqrexlemga  11449  resqrexlemsqa  11450  resqrexlemex  11451  resqrex  11452  sqrtdiv  11468  absvalsq  11479  absreimsq  11493  absdivap  11496  cau3lem  11540  maxabslemlub  11633  maxabslemval  11634  max0addsup  11645  minabs  11662  bdtrilem  11665  bdtri  11666  xrmaxaddlem  11686  xrmaxadd  11687  xrbdtri  11702  clim  11707  clim2  11709  climshftlemg  11728  climshft2  11732  climcn1  11734  climcn2  11735  subcn2  11737  reccn2ap  11739  climmulc2  11757  climsubc2  11759  clim2ser  11763  iser3shft  11772  climcau  11773  serf0  11778  fzosump1  11843  fsum1p  11844  fsump1  11846  sumsplitdc  11858  fsump1i  11859  mptfzshft  11868  fisum0diag2  11873  fsumconst  11880  fsumdifsnconst  11881  modfsummodlemstep  11883  modfsummod  11884  telfsumo  11892  fsumparts  11896  fsumrelem  11897  hash2iun1dif1  11906  binomlem  11909  binom  11910  binom1p  11911  binom1dif  11913  bcxmas  11915  isumsplit  11917  isum1p  11918  arisum  11924  arisum2  11925  trireciplem  11926  geoserap  11933  geolim  11937  geolim2  11938  georeclim  11939  geo2sum  11940  geoisum1  11945  cvgratnnlemseq  11952  cvgratnnlemsumlt  11954  cvgratnnlemfm  11955  cvgratz  11958  mertenslemi1  11961  mertenslem2  11962  mertensabs  11963  fprod1p  12025  fprodp1  12026  fprodcl2lem  12031  fprodfac  12041  fprodeq0  12043  fprodconst  12046  fprodrec  12055  fprodsplit1f  12060  fprodmodd  12067  efcllemp  12084  ef0lem  12086  efval  12087  esum  12088  ege2le3  12097  efaddlem  12100  efsep  12117  effsumlt  12118  eft0val  12119  efgt1p2  12121  efgt1p  12122  sinval  12128  cosval  12129  resinval  12141  recosval  12142  efi4p  12143  resin4p  12144  recos4p  12145  sinneg  12152  cosneg  12153  efival  12158  sinadd  12162  cosadd  12163  tanaddap  12165  sinmul  12170  cosmul  12171  cos2t  12176  cos2tsin  12177  ef01bndlem  12182  absefib  12197  demoivre  12199  demoivreALT  12200  eirraplem  12203  p1modz1  12220  dvdsmodexp  12221  moddvds  12225  mulmoddvds  12289  3dvds2dec  12292  zeo3  12294  odd2np1lem  12298  odd2np1  12299  oexpneg  12303  2tp1odd  12310  ltoddhalfle  12319  opoe  12321  opeo  12323  omeo  12324  m1expo  12326  m1exp1  12327  nn0o1gt2  12331  nn0o  12333  divalglemnn  12344  divalglemqt  12345  divalglemeunn  12347  divalglemex  12348  divalglemeuneg  12349  flodddiv4  12362  flodddiv4t2lthalf  12365  bitsp1o  12379  bitsmod  12382  bitsinv1lem  12387  gcdaddm  12420  bezoutlemnewy  12432  bezoutlema  12435  bezoutlemb  12436  bezoutlemex  12437  bezoutlemaz  12439  mulgcd  12452  gcddiv  12455  gcdmultiplez  12457  rpmulgcd  12462  rplpwr  12463  uzwodc  12473  lcmgcdlem  12514  lcmgcd  12515  divgcdcoprmex  12539  cncongr2  12541  prmexpb  12588  rpexp  12590  rpexp1i  12591  sqrt2irrlem  12598  oddpwdclemxy  12606  oddpwdclemndvds  12608  sqpweven  12612  2sqpwodd  12613  sqne2sq  12614  qmuldeneqnum  12632  nn0gcdsq  12637  zgcdsq  12638  numdensq  12639  dfphi2  12657  phiprmpw  12659  phiprm  12660  eulerthlema  12667  eulerthlemh  12668  eulerthlemth  12669  fermltl  12671  prmdiv  12672  prmdiveq  12673  prmdivdiv  12674  hashgcdlem  12675  odzval  12679  odzcllem  12680  odzdvds  12683  vfermltl  12689  powm2modprm  12690  reumodprminv  12691  modprm0  12692  nnnn0modprm0  12693  modprmn0modprm0  12694  coprimeprodsq  12695  coprimeprodsq2  12696  pythagtriplem1  12703  pythagtriplem3  12705  pythagtriplem4  12706  pythagtriplem6  12708  pythagtriplem7  12709  pythagtriplem12  12713  pythagtriplem14  12715  pythagtriplem15  12716  pythagtriplem16  12717  pythagtriplem17  12718  pythagtriplem18  12719  pceu  12733  pczpre  12735  pcdiv  12740  pcqdiv  12745  pcrec  12746  pczndvds  12754  pcneg  12763  pc2dvds  12768  pcprmpw2  12771  pcaddlem  12777  pcadd  12778  fldivp1  12786  pockthlem  12794  pockthi  12796  4sqlem5  12820  4sqlem9  12824  4sqlem10  12825  4sqlem2  12827  4sqlem3  12828  4sqlem4  12830  mul4sqlem  12831  4sqlem11  12839  4sqlem12  12840  4sqlem14  12842  4sqlem15  12843  4sqlem17  12845  4sqlem19  12847  ennnfonelemkh  12898  ennnfonelemhf1o  12899  setscomd  12988  ressressg  13022  qusex  13272  qusin  13273  grpinvalem  13332  grpinva  13333  grprida  13334  gsumsplit1r  13345  isnsgrp  13353  sgrpass  13355  sgrp1  13358  sgrppropd  13360  prdssgrpd  13362  mnd12g  13375  mndpropd  13387  prdsidlem  13394  prdsmndd  13395  imasmnd2  13399  mhmex  13409  mhmlin  13414  grprcan  13484  grpinvid1  13499  isgrpinv  13501  grplcan  13509  grpasscan1  13510  grplmulf1o  13521  grpinvadd  13525  grpinvsub  13529  grpsubsub4  13540  grppnpcan2  13541  grpnpncan  13542  dfgrp3mlem  13545  dfgrp3m  13546  grplactcnv  13549  prdsinvlem  13555  imasgrp2  13561  mhmlem  13565  mhmid  13566  mhmmnd  13567  mulgnnp1  13581  mulg2  13582  mulgnn0p1  13584  mulgsubcl  13587  mulgneg  13591  mulgaddcomlem  13596  mulgaddcom  13597  mulgz  13601  mulgnn0dir  13603  mulgdirlem  13604  mulgdir  13605  mulgneg2  13607  mulgnnass  13608  mulgnn0ass  13609  mulgass  13610  mulgassr  13611  mulgmodid  13612  mulgsubdir  13613  submmulg  13617  isnsg3  13658  nmzsubg  13661  ssnmz  13662  0nsg  13665  eqger  13675  eqgid  13677  eqgcpbl  13679  ghmlin  13699  ghmmulg  13707  ghmnsgima  13719  ghmnsgpreima  13720  conjghm  13727  conjnmz  13730  ablsub2inv  13762  abladdsub4  13765  abladdsub  13766  ablpncan2  13767  ablpnpcan  13771  ablnncan  13772  ablnnncan1  13775  gsumfzconst  13792  gsumfzsnfd  13796  mgpress  13808  rngass  13816  rngdi  13817  rngdir  13818  rnglz  13822  rngmneg1  13824  rngsubdir  13829  rngpropd  13832  imasrng  13833  srgass  13848  srgmulgass  13866  srgpcomp  13867  srgpcompp  13868  srgpcomppsc  13869  ringpropd  13915  ringlz  13920  ring1eq0  13925  ringnegl  13928  ringmneg1  13930  ringsubdir  13934  mulgass2  13935  ring1  13936  imasring  13941  opprrng  13954  opprring  13956  unitgrp  13993  dvrcan1  14017  rdivmuldivd  14021  subrginv  14114  resrhm  14125  unitrrg  14144  islmod  14168  lmodlema  14169  islmodd  14170  lmod0vs  14198  lmodvs0  14199  lmodvsmmulgdi  14200  lmodvneg1  14207  lmodvsneg  14208  lmodsubvs  14220  lmodsubdi  14221  lmodsubdir  14222  lmodprop2d  14225  rmodislmodlem  14227  rmodislmod  14228  lsssetm  14233  islssmd  14236  lssclg  14241  lssvacl  14242  lss1d  14260  lsspropdg  14308  sraval  14314  rnglidlmcl  14357  gsumfzfsumlemm  14464  znunit  14536  mplsubgfilemcl  14576  resttop  14757  restco  14761  restin  14763  lmfval  14779  cnprcl2k  14793  txrest  14863  txdis1cn  14865  cnmpt2res  14884  psmettri2  14915  psmettri  14917  xmettri2  14948  xmettri  14959  mettri  14960  metrtri  14964  blvalps  14975  blval  14976  xblss2  14992  blhalf  14995  comet  15086  xmetxp  15094  txmetcnp  15105  cnmet  15117  ioo2bl  15138  ivthreinc  15232  limcmpted  15250  limcimolemlt  15251  cnplimclemr  15256  limccnp2cntop  15264  reldvg  15266  dvfvalap  15268  dvidlemap  15278  dvidrelem  15279  dvidsslem  15280  dvconst  15281  dvconstre  15283  dvconstss  15285  dvcnp2cntop  15286  dvaddxxbr  15288  dvmulxxbr  15289  dvcoapbr  15294  dvcjbr  15295  dvexp  15298  dvrecap  15300  dvmptcmulcn  15308  dveflem  15313  plyval  15319  elply2  15322  elplyr  15327  elplyd  15328  ply1termlem  15329  plyaddlem1  15334  plymullem1  15335  plycoeid3  15344  plycjlemc  15347  dvply1  15352  sin0pilem1  15368  sinperlem  15395  ptolemy  15411  tangtx  15425  abssinper  15433  reexplog  15458  relogexp  15459  cxprec  15497  rpdivcxp  15498  cxpmul  15499  rpabscxpbnd  15527  rplogbval  15532  rplogbreexp  15540  rprelogbmul  15542  logbrec  15547  logbgcd1irraplemap  15556  binom4  15566  wilthlem1  15567  mpodvdsmulf1o  15577  sgmppw  15579  0sgmppw  15580  1sgmprm  15581  1sgm2ppw  15582  perfectlem1  15586  perfectlem2  15587  perfect  15588  lgslem1  15592  lgslem4  15595  lgsval  15596  lgsfvalg  15597  lgsval2lem  15602  lgsval4lem  15603  lgsvalmod  15611  lgsneg  15616  lgsneg1  15617  lgsmod  15618  lgsdilem  15619  lgsdir2lem4  15623  lgsdir2  15625  lgsdirprm  15626  lgsdir  15627  lgsne0  15630  lgssq  15632  lgssq2  15633  lgsmulsqcoprm  15638  lgsdirnn0  15639  lgsdinn0  15640  gausslemma2dlem1a  15650  gausslemma2dlem4  15656  gausslemma2dlem5a  15657  gausslemma2dlem5  15658  gausslemma2dlem6  15659  gausslemma2dlem7  15660  gausslemma2d  15661  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisenlem4  15665  lgseisen  15666  lgsquadlem1  15669  lgsquadlem2  15670  lgsquad2lem1  15673  lgsquad2lem2  15674  lgsquad3  15676  m1lgs  15677  2lgslem1a  15680  2lgslem1c  15682  2lgslem3a  15685  2lgslem3b  15686  2lgslem3c  15687  2lgslem3d  15688  2lgslem3a1  15689  2lgslem3b1  15690  2lgslem3c1  15691  2lgslem3d1  15692  2lgsoddprmlem1  15697  2lgsoddprmlem2  15698  2lgsoddprmlem3  15703  2sqlem1  15706  2sqlem2  15707  mul2sq  15708  2sqlem3  15709  2sqlem4  15710  2sqlem8  15715  2sqlem9  15716  2sqlem10  15717  trilpolemeq1  16181  trilpolemlt1  16182  trirec0xor  16186  apdifflemf  16187  apdiff  16189