Theorem oveq1d 5958

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

Syntax hints:   → wi 4   = wceq 1372  (class class class)co 5943

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-rex 2489  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-uni 3850  df-br 4044  df-iota 5231  df-fv 5278  df-ov 5946

This theorem is referenced by:  fvoveq1d  5965  csbov2g  5985  caovassg  6104  caovdig  6120  caovdirg  6123  caov12d  6127  caov31d  6128  caov411d  6131  caofinvl  6183  omsuc  6557  nnmsucr  6573  nnm1  6610  nnm2  6611  ecovass  6730  ecoviass  6731  ecovdi  6732  ecovidi  6733  isacnm  7314  addasspig  7442  mulasspig  7444  mulpipq2  7483  distrnqg  7499  ltsonq  7510  ltanqg  7512  ltmnqg  7513  ltexnqq  7520  archnqq  7529  prarloclemarch2  7531  enq0sym  7544  addnq0mo  7559  mulnq0mo  7560  addnnnq0  7561  nqpnq0nq  7565  nq0m0r  7568  nq0a0  7569  nnanq0  7570  distrnq0  7571  addassnq0  7574  addpinq1  7576  prarloclemlo  7606  prarloclem3  7609  prarloclem5  7612  prarloclemcalc  7614  addnqprllem  7639  addnqprulem  7640  appdivnq  7675  recexprlem1ssl  7745  recexprlem1ssu  7746  ltmprr  7754  cauappcvgprlemladdru  7768  cauappcvgprlem1  7771  caucvgprlemnkj  7778  caucvgprlemnbj  7779  caucvgprlemcl  7788  caucvgprlemladdfu  7789  caucvgprlemladdrl  7790  caucvgprlem1  7791  caucvgprprlemcbv  7799  caucvgprprlemval  7800  caucvgprprlemexb  7819  caucvgprprlem1  7821  addcmpblnr  7851  mulcmpblnrlemg  7852  addsrmo  7855  mulsrmo  7856  addsrpr  7857  mulsrpr  7858  ltsrprg  7859  1idsr  7880  pn0sr  7883  recexgt0sr  7885  mulgt0sr  7890  srpospr  7895  prsradd  7898  caucvgsrlemfv  7903  caucvgsrlemcau  7905  caucvgsrlemgt1  7907  caucvgsrlemoffval  7908  caucvgsrlemoffcau  7910  caucvgsrlemoffres  7912  caucvgsrlembnd  7913  caucvgsr  7914  map2psrprg  7917  pitonnlem1p1  7958  pitonnlem2  7959  pitonn  7960  recidpirqlemcalc  7969  ax1rid  7989  axrnegex  7991  axcnre  7993  recriota  8002  nntopi  8006  axcaucvglemval  8009  axcaucvglemcau  8010  axcaucvglemres  8011  mul12  8200  mul4  8203  muladd11  8204  readdcan  8211  muladd11r  8227  add12  8229  cnegex  8249  addcan  8251  negeu  8262  pncan2  8278  addsubass  8281  addsub  8282  2addsub  8285  addsubeq4  8286  subid  8290  subid1  8291  npncan  8292  nppcan  8293  nnpcan  8294  nnncan1  8307  npncan3  8309  pnpcan  8310  pnncan  8312  ppncan  8313  addsub4  8314  negsub  8319  subneg  8320  subeqxfrd  8434  mvlraddd  8435  mvlladdd  8436  mvrraddd  8437  subaddeqd  8440  ine0  8465  mulneg1  8466  ltadd2  8491  apreap  8659  cru  8674  recexap  8725  mulcanapd  8733  div23ap  8763  div13ap  8765  divmulassap  8767  divmulasscomap  8768  divcanap4  8771  muldivdirap  8779  divsubdirap  8780  divmuldivap  8784  divdivdivap  8785  divcanap5  8786  divmul13ap  8787  divmuleqap  8789  divdiv32ap  8792  divcanap7  8793  dmdcanap  8794  divdivap1  8795  divdivap2  8796  divadddivap  8799  divsubdivap  8800  conjmulap  8801  divneg2ap  8808  subrecap  8911  mvllmulapd  8914  lt2mul2div  8951  nndivtr  9077  2halves  9265  halfaddsub  9270  subhalfhalf  9271  avgle1  9277  avgle2  9278  div4p1lem1div2  9290  un0addcl  9327  un0mulcl  9328  peano2z  9407  zneo  9473  nneoor  9474  nneo  9475  zeo  9477  zeo2  9478  deceq1  9507  qreccl  9762  xaddcom  9982  xnegdi  9989  xaddass  9990  xaddass2  9991  xpncan  9992  xleadd1a  9994  xltadd1  9997  xposdif  10003  xadd4d  10006  lincmb01cmp  10124  iccf1o  10125  fz0to4untppr  10245  fzo0addel  10315  fzosubel3  10323  qavgle  10399  2tnp1ge0ge0  10442  fldiv4p1lem1div2  10446  fldiv4lem1div2  10448  ceilqm1lt  10455  flqdiv  10464  modqlt  10476  modqdiffl  10478  modqcyc2  10503  modqaddabs  10505  mulqaddmodid  10507  mulp1mod1  10508  modqmuladd  10509  modqmuladdnn0  10511  qnegmod  10512  addmodid  10515  addmodidr  10516  modqadd2mod  10517  modqm1p1mod0  10518  modqmul12d  10521  modqnegd  10522  modqadd12d  10523  modqsub12d  10524  q2submod  10528  modqmulmodr  10533  modqaddmulmod  10534  modqsubdir  10536  modfzo0difsn  10538  modsumfzodifsn  10539  addmodlteq  10541  frecuzrdgsuc  10557  frecfzennn  10569  iseqovex  10601  seq3-1p  10633  seq3caopr2  10636  seqcaopr2g  10637  seq3caopr  10638  seqcaoprg  10639  seqf1oglem2a  10661  seqf1oglem1  10662  seqf1oglem2  10663  seq3id  10668  seq3homo  10670  seq3z  10671  seqhomog  10673  seqfeq4g  10674  expp1  10689  exprecap  10723  expaddzaplem  10725  expmulzap  10728  expdivap  10733  sqval  10740  sqsubswap  10742  sqdividap  10747  subsq  10789  subsq2  10790  binom2  10794  binom2sub  10796  mulbinom2  10799  binom3  10800  zesq  10801  bernneq2  10804  modqexp  10809  sqoddm1div8  10836  mulsubdivbinom2ap  10854  nn0opthlem1d  10863  nn0opthd  10865  nn0opth2d  10866  facp1  10873  facdiv  10881  facndiv  10882  faclbnd  10884  faclbnd2  10885  faclbnd3  10886  bcval  10892  bccmpl  10897  bcm1k  10903  bcp1n  10904  bcp1nk  10905  bcval5  10906  bcp1m1  10908  bcpasc  10909  bcn2m1  10912  hashprg  10951  hashdifpr  10963  hashfzo  10965  hashfzp1  10967  hashfz0  10968  hashxp  10969  zfz1isolemsplit  10981  zfz1isolem1  10983  seq3coll  10985  lswwrd  11038  ccatfvalfi  11046  ccatass  11062  lswccatn0lsw  11065  reval  11131  crre  11139  remim  11142  remul2  11155  immul2  11162  imval2  11176  cjdivap  11191  caucvgre  11263  cvg1nlemcau  11266  cvg1nlemres  11267  resqrexlemp1rp  11288  resqrexlemfp1  11291  resqrexlemover  11292  resqrexlemcalc1  11296  resqrexlemcalc3  11298  resqrexlemnm  11300  resqrexlemoverl  11303  resqrexlemglsq  11304  resqrexlemga  11305  resqrexlemsqa  11306  resqrexlemex  11307  resqrex  11308  sqrtdiv  11324  absvalsq  11335  absreimsq  11349  absdivap  11352  cau3lem  11396  maxabslemlub  11489  maxabslemval  11490  max0addsup  11501  minabs  11518  bdtrilem  11521  bdtri  11522  xrmaxaddlem  11542  xrmaxadd  11543  xrbdtri  11558  clim  11563  clim2  11565  climshftlemg  11584  climshft2  11588  climcn1  11590  climcn2  11591  subcn2  11593  reccn2ap  11595  climmulc2  11613  climsubc2  11615  clim2ser  11619  iser3shft  11628  climcau  11629  serf0  11634  fzosump1  11699  fsum1p  11700  fsump1  11702  sumsplitdc  11714  fsump1i  11715  mptfzshft  11724  fisum0diag2  11729  fsumconst  11736  fsumdifsnconst  11737  modfsummodlemstep  11739  modfsummod  11740  telfsumo  11748  fsumparts  11752  fsumrelem  11753  hash2iun1dif1  11762  binomlem  11765  binom  11766  binom1p  11767  binom1dif  11769  bcxmas  11771  isumsplit  11773  isum1p  11774  arisum  11780  arisum2  11781  trireciplem  11782  geoserap  11789  geolim  11793  geolim2  11794  georeclim  11795  geo2sum  11796  geoisum1  11801  cvgratnnlemseq  11808  cvgratnnlemsumlt  11810  cvgratnnlemfm  11811  cvgratz  11814  mertenslemi1  11817  mertenslem2  11818  mertensabs  11819  fprod1p  11881  fprodp1  11882  fprodcl2lem  11887  fprodfac  11897  fprodeq0  11899  fprodconst  11902  fprodrec  11911  fprodsplit1f  11916  fprodmodd  11923  efcllemp  11940  ef0lem  11942  efval  11943  esum  11944  ege2le3  11953  efaddlem  11956  efsep  11973  effsumlt  11974  eft0val  11975  efgt1p2  11977  efgt1p  11978  sinval  11984  cosval  11985  resinval  11997  recosval  11998  efi4p  11999  resin4p  12000  recos4p  12001  sinneg  12008  cosneg  12009  efival  12014  sinadd  12018  cosadd  12019  tanaddap  12021  sinmul  12026  cosmul  12027  cos2t  12032  cos2tsin  12033  ef01bndlem  12038  absefib  12053  demoivre  12055  demoivreALT  12056  eirraplem  12059  p1modz1  12076  dvdsmodexp  12077  moddvds  12081  mulmoddvds  12145  3dvds2dec  12148  zeo3  12150  odd2np1lem  12154  odd2np1  12155  oexpneg  12159  2tp1odd  12166  ltoddhalfle  12175  opoe  12177  opeo  12179  omeo  12180  m1expo  12182  m1exp1  12183  nn0o1gt2  12187  nn0o  12189  divalglemnn  12200  divalglemqt  12201  divalglemeunn  12203  divalglemex  12204  divalglemeuneg  12205  flodddiv4  12218  flodddiv4t2lthalf  12221  bitsp1o  12235  bitsmod  12238  bitsinv1lem  12243  gcdaddm  12276  bezoutlemnewy  12288  bezoutlema  12291  bezoutlemb  12292  bezoutlemex  12293  bezoutlemaz  12295  mulgcd  12308  gcddiv  12311  gcdmultiplez  12313  rpmulgcd  12318  rplpwr  12319  uzwodc  12329  lcmgcdlem  12370  lcmgcd  12371  divgcdcoprmex  12395  cncongr2  12397  prmexpb  12444  rpexp  12446  rpexp1i  12447  sqrt2irrlem  12454  oddpwdclemxy  12462  oddpwdclemndvds  12464  sqpweven  12468  2sqpwodd  12469  sqne2sq  12470  qmuldeneqnum  12488  nn0gcdsq  12493  zgcdsq  12494  numdensq  12495  dfphi2  12513  phiprmpw  12515  phiprm  12516  eulerthlema  12523  eulerthlemh  12524  eulerthlemth  12525  fermltl  12527  prmdiv  12528  prmdiveq  12529  prmdivdiv  12530  hashgcdlem  12531  odzval  12535  odzcllem  12536  odzdvds  12539  vfermltl  12545  powm2modprm  12546  reumodprminv  12547  modprm0  12548  nnnn0modprm0  12549  modprmn0modprm0  12550  coprimeprodsq  12551  coprimeprodsq2  12552  pythagtriplem1  12559  pythagtriplem3  12561  pythagtriplem4  12562  pythagtriplem6  12564  pythagtriplem7  12565  pythagtriplem12  12569  pythagtriplem14  12571  pythagtriplem15  12572  pythagtriplem16  12573  pythagtriplem17  12574  pythagtriplem18  12575  pceu  12589  pczpre  12591  pcdiv  12596  pcqdiv  12601  pcrec  12602  pczndvds  12610  pcneg  12619  pc2dvds  12624  pcprmpw2  12627  pcaddlem  12633  pcadd  12634  fldivp1  12642  pockthlem  12650  pockthi  12652  4sqlem5  12676  4sqlem9  12680  4sqlem10  12681  4sqlem2  12683  4sqlem3  12684  4sqlem4  12686  mul4sqlem  12687  4sqlem11  12695  4sqlem12  12696  4sqlem14  12698  4sqlem15  12699  4sqlem17  12701  4sqlem19  12703  ennnfonelemkh  12754  ennnfonelemhf1o  12755  setscomd  12844  ressressg  12878  qusex  13128  qusin  13129  grpinvalem  13188  grpinva  13189  grprida  13190  gsumsplit1r  13201  isnsgrp  13209  sgrpass  13211  sgrp1  13214  sgrppropd  13216  prdssgrpd  13218  mnd12g  13231  mndpropd  13243  prdsidlem  13250  prdsmndd  13251  imasmnd2  13255  mhmex  13265  mhmlin  13270  grprcan  13340  grpinvid1  13355  isgrpinv  13357  grplcan  13365  grpasscan1  13366  grplmulf1o  13377  grpinvadd  13381  grpinvsub  13385  grpsubsub4  13396  grppnpcan2  13397  grpnpncan  13398  dfgrp3mlem  13401  dfgrp3m  13402  grplactcnv  13405  prdsinvlem  13411  imasgrp2  13417  mhmlem  13421  mhmid  13422  mhmmnd  13423  mulgnnp1  13437  mulg2  13438  mulgnn0p1  13440  mulgsubcl  13443  mulgneg  13447  mulgaddcomlem  13452  mulgaddcom  13453  mulgz  13457  mulgnn0dir  13459  mulgdirlem  13460  mulgdir  13461  mulgneg2  13463  mulgnnass  13464  mulgnn0ass  13465  mulgass  13466  mulgassr  13467  mulgmodid  13468  mulgsubdir  13469  submmulg  13473  isnsg3  13514  nmzsubg  13517  ssnmz  13518  0nsg  13521  eqger  13531  eqgid  13533  eqgcpbl  13535  ghmlin  13555  ghmmulg  13563  ghmnsgima  13575  ghmnsgpreima  13576  conjghm  13583  conjnmz  13586  ablsub2inv  13618  abladdsub4  13621  abladdsub  13622  ablpncan2  13623  ablpnpcan  13627  ablnncan  13628  ablnnncan1  13631  gsumfzconst  13648  gsumfzsnfd  13652  mgpress  13664  rngass  13672  rngdi  13673  rngdir  13674  rnglz  13678  rngmneg1  13680  rngsubdir  13685  rngpropd  13688  imasrng  13689  srgass  13704  srgmulgass  13722  srgpcomp  13723  srgpcompp  13724  srgpcomppsc  13725  ringpropd  13771  ringlz  13776  ring1eq0  13781  ringnegl  13784  ringmneg1  13786  ringsubdir  13790  mulgass2  13791  ring1  13792  imasring  13797  opprrng  13810  opprring  13812  unitgrp  13849  dvrcan1  13873  rdivmuldivd  13877  subrginv  13970  resrhm  13981  unitrrg  14000  islmod  14024  lmodlema  14025  islmodd  14026  lmod0vs  14054  lmodvs0  14055  lmodvsmmulgdi  14056  lmodvneg1  14063  lmodvsneg  14064  lmodsubvs  14076  lmodsubdi  14077  lmodsubdir  14078  lmodprop2d  14081  rmodislmodlem  14083  rmodislmod  14084  lsssetm  14089  islssmd  14092  lssclg  14097  lssvacl  14098  lss1d  14116  lsspropdg  14164  sraval  14170  rnglidlmcl  14213  gsumfzfsumlemm  14320  znunit  14392  mplsubgfilemcl  14432  resttop  14613  restco  14617  restin  14619  lmfval  14635  cnprcl2k  14649  txrest  14719  txdis1cn  14721  cnmpt2res  14740  psmettri2  14771  psmettri  14773  xmettri2  14804  xmettri  14815  mettri  14816  metrtri  14820  blvalps  14831  blval  14832  xblss2  14848  blhalf  14851  comet  14942  xmetxp  14950  txmetcnp  14961  cnmet  14973  ioo2bl  14994  ivthreinc  15088  limcmpted  15106  limcimolemlt  15107  cnplimclemr  15112  limccnp2cntop  15120  reldvg  15122  dvfvalap  15124  dvidlemap  15134  dvidrelem  15135  dvidsslem  15136  dvconst  15137  dvconstre  15139  dvconstss  15141  dvcnp2cntop  15142  dvaddxxbr  15144  dvmulxxbr  15145  dvcoapbr  15150  dvcjbr  15151  dvexp  15154  dvrecap  15156  dvmptcmulcn  15164  dveflem  15169  plyval  15175  elply2  15178  elplyr  15183  elplyd  15184  ply1termlem  15185  plyaddlem1  15190  plymullem1  15191  plycoeid3  15200  plycjlemc  15203  dvply1  15208  sin0pilem1  15224  sinperlem  15251  ptolemy  15267  tangtx  15281  abssinper  15289  reexplog  15314  relogexp  15315  cxprec  15353  rpdivcxp  15354  cxpmul  15355  rpabscxpbnd  15383  rplogbval  15388  rplogbreexp  15396  rprelogbmul  15398  logbrec  15403  logbgcd1irraplemap  15412  binom4  15422  wilthlem1  15423  mpodvdsmulf1o  15433  sgmppw  15435  0sgmppw  15436  1sgmprm  15437  1sgm2ppw  15438  perfectlem1  15442  perfectlem2  15443  perfect  15444  lgslem1  15448  lgslem4  15451  lgsval  15452  lgsfvalg  15453  lgsval2lem  15458  lgsval4lem  15459  lgsvalmod  15467  lgsneg  15472  lgsneg1  15473  lgsmod  15474  lgsdilem  15475  lgsdir2lem4  15479  lgsdir2  15481  lgsdirprm  15482  lgsdir  15483  lgsne0  15486  lgssq  15488  lgssq2  15489  lgsmulsqcoprm  15494  lgsdirnn0  15495  lgsdinn0  15496  gausslemma2dlem1a  15506  gausslemma2dlem4  15512  gausslemma2dlem5a  15513  gausslemma2dlem5  15514  gausslemma2dlem6  15515  gausslemma2dlem7  15516  gausslemma2d  15517  lgseisenlem1  15518  lgseisenlem2  15519  lgseisenlem3  15520  lgseisenlem4  15521  lgseisen  15522  lgsquadlem1  15525  lgsquadlem2  15526  lgsquad2lem1  15529  lgsquad2lem2  15530  lgsquad3  15532  m1lgs  15533  2lgslem1a  15536  2lgslem1c  15538  2lgslem3a  15541  2lgslem3b  15542  2lgslem3c  15543  2lgslem3d  15544  2lgslem3a1  15545  2lgslem3b1  15546  2lgslem3c1  15547  2lgslem3d1  15548  2lgsoddprmlem1  15553  2lgsoddprmlem2  15554  2lgsoddprmlem3  15559  2sqlem1  15562  2sqlem2  15563  mul2sq  15564  2sqlem3  15565  2sqlem4  15566  2sqlem8  15571  2sqlem9  15572  2sqlem10  15573  trilpolemeq1  15941  trilpolemlt1  15942  trirec0xor  15946  apdifflemf  15947  apdiff  15949