Theorem oveq1d 6028

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

Syntax hints:   → wi 4   = wceq 1395  (class class class)co 6013

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-rex 2514  df-v 2802  df-un 3202  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-iota 5284  df-fv 5332  df-ov 6016

This theorem is referenced by:  fvoveq1d  6035  csbov2g  6055  caovassg  6176  caovdig  6192  caovdirg  6195  caov12d  6199  caov31d  6200  caov411d  6203  caofinvl  6256  omsuc  6635  nnmsucr  6651  nnm1  6688  nnm2  6689  ecovass  6808  ecoviass  6809  ecovdi  6810  ecovidi  6811  isacnm  7408  addasspig  7540  mulasspig  7542  mulpipq2  7581  distrnqg  7597  ltsonq  7608  ltanqg  7610  ltmnqg  7611  ltexnqq  7618  archnqq  7627  prarloclemarch2  7629  enq0sym  7642  addnq0mo  7657  mulnq0mo  7658  addnnnq0  7659  nqpnq0nq  7663  nq0m0r  7666  nq0a0  7667  nnanq0  7668  distrnq0  7669  addassnq0  7672  addpinq1  7674  prarloclemlo  7704  prarloclem3  7707  prarloclem5  7710  prarloclemcalc  7712  addnqprllem  7737  addnqprulem  7738  appdivnq  7773  recexprlem1ssl  7843  recexprlem1ssu  7844  ltmprr  7852  cauappcvgprlemladdru  7866  cauappcvgprlem1  7869  caucvgprlemnkj  7876  caucvgprlemnbj  7877  caucvgprlemcl  7886  caucvgprlemladdfu  7887  caucvgprlemladdrl  7888  caucvgprlem1  7889  caucvgprprlemcbv  7897  caucvgprprlemval  7898  caucvgprprlemexb  7917  caucvgprprlem1  7919  addcmpblnr  7949  mulcmpblnrlemg  7950  addsrmo  7953  mulsrmo  7954  addsrpr  7955  mulsrpr  7956  ltsrprg  7957  1idsr  7978  pn0sr  7981  recexgt0sr  7983  mulgt0sr  7988  srpospr  7993  prsradd  7996  caucvgsrlemfv  8001  caucvgsrlemcau  8003  caucvgsrlemgt1  8005  caucvgsrlemoffval  8006  caucvgsrlemoffcau  8008  caucvgsrlemoffres  8010  caucvgsrlembnd  8011  caucvgsr  8012  map2psrprg  8015  pitonnlem1p1  8056  pitonnlem2  8057  pitonn  8058  recidpirqlemcalc  8067  ax1rid  8087  axrnegex  8089  axcnre  8091  recriota  8100  nntopi  8104  axcaucvglemval  8107  axcaucvglemcau  8108  axcaucvglemres  8109  mul12  8298  mul4  8301  muladd11  8302  readdcan  8309  muladd11r  8325  add12  8327  cnegex  8347  addcan  8349  negeu  8360  pncan2  8376  addsubass  8379  addsub  8380  2addsub  8383  addsubeq4  8384  subid  8388  subid1  8389  npncan  8390  nppcan  8391  nnpcan  8392  nnncan1  8405  npncan3  8407  pnpcan  8408  pnncan  8410  ppncan  8411  addsub4  8412  negsub  8417  subneg  8418  subeqxfrd  8532  mvlraddd  8533  mvlladdd  8534  mvrraddd  8535  subaddeqd  8538  ine0  8563  mulneg1  8564  ltadd2  8589  apreap  8757  cru  8772  recexap  8823  mulcanapd  8831  div23ap  8861  div13ap  8863  divmulassap  8865  divmulasscomap  8866  divcanap4  8869  muldivdirap  8877  divsubdirap  8878  divmuldivap  8882  divdivdivap  8883  divcanap5  8884  divmul13ap  8885  divmuleqap  8887  divdiv32ap  8890  divcanap7  8891  dmdcanap  8892  divdivap1  8893  divdivap2  8894  divadddivap  8897  divsubdivap  8898  conjmulap  8899  divneg2ap  8906  subrecap  9009  mvllmulapd  9012  lt2mul2div  9049  nndivtr  9175  2halves  9363  halfaddsub  9368  subhalfhalf  9369  avgle1  9375  avgle2  9376  div4p1lem1div2  9388  un0addcl  9425  un0mulcl  9426  peano2z  9505  zneo  9571  nneoor  9572  nneo  9573  zeo  9575  zeo2  9576  deceq1  9605  qreccl  9866  xaddcom  10086  xnegdi  10093  xaddass  10094  xaddass2  10095  xpncan  10096  xleadd1a  10098  xltadd1  10101  xposdif  10107  xadd4d  10110  lincmb01cmp  10228  iccf1o  10229  fz0to4untppr  10349  fzo0addel  10423  fzosubel3  10431  qavgle  10508  2tnp1ge0ge0  10551  fldiv4p1lem1div2  10555  fldiv4lem1div2  10557  ceilqm1lt  10564  flqdiv  10573  modqlt  10585  modqdiffl  10587  modqcyc2  10612  modqaddabs  10614  mulqaddmodid  10616  mulp1mod1  10617  modqmuladd  10618  modqmuladdnn0  10620  qnegmod  10621  addmodid  10624  addmodidr  10625  modqadd2mod  10626  modqm1p1mod0  10627  modqmul12d  10630  modqnegd  10631  modqadd12d  10632  modqsub12d  10633  q2submod  10637  modqmulmodr  10642  modqaddmulmod  10643  modqsubdir  10645  modfzo0difsn  10647  modsumfzodifsn  10648  addmodlteq  10650  frecuzrdgsuc  10666  frecfzennn  10678  iseqovex  10710  seq3-1p  10742  seq3caopr2  10745  seqcaopr2g  10746  seq3caopr  10747  seqcaoprg  10748  seqf1oglem2a  10770  seqf1oglem1  10771  seqf1oglem2  10772  seq3id  10777  seq3homo  10779  seq3z  10780  seqhomog  10782  seqfeq4g  10783  expp1  10798  exprecap  10832  expaddzaplem  10834  expmulzap  10837  expdivap  10842  sqval  10849  sqsubswap  10851  sqdividap  10856  subsq  10898  subsq2  10899  binom2  10903  binom2sub  10905  mulbinom2  10908  binom3  10909  zesq  10910  bernneq2  10913  modqexp  10918  sqoddm1div8  10945  mulsubdivbinom2ap  10963  nn0opthlem1d  10972  nn0opthd  10974  nn0opth2d  10975  facp1  10982  facdiv  10990  facndiv  10991  faclbnd  10993  faclbnd2  10994  faclbnd3  10995  bcval  11001  bccmpl  11006  bcm1k  11012  bcp1n  11013  bcp1nk  11014  bcval5  11015  bcp1m1  11017  bcpasc  11018  bcn2m1  11021  hashprg  11062  hashdifpr  11074  hashfzo  11076  hashfzp1  11078  hashfz0  11079  hashxp  11080  zfz1isolemsplit  11092  zfz1isolem1  11094  seq3coll  11096  lswwrd  11150  ccatfvalfi  11159  ccatass  11175  lswccatn0lsw  11178  wrdlenccats1lenm1g  11203  ccatw2s1leng  11205  ccatswrd  11241  ccatpfx  11272  swrdpfx  11278  pfxpfx  11279  ccats1pfxeq  11285  wrdeqs1cat  11291  wrdind  11293  wrd2ind  11294  pfxccatpfx2  11308  pfxccatin12d  11316  cats1catd  11339  cats2catd  11340  s2leng  11360  reval  11400  crre  11408  remim  11411  remul2  11424  immul2  11431  imval2  11445  cjdivap  11460  caucvgre  11532  cvg1nlemcau  11535  cvg1nlemres  11536  resqrexlemp1rp  11557  resqrexlemfp1  11560  resqrexlemover  11561  resqrexlemcalc1  11565  resqrexlemcalc3  11567  resqrexlemnm  11569  resqrexlemoverl  11572  resqrexlemglsq  11573  resqrexlemga  11574  resqrexlemsqa  11575  resqrexlemex  11576  resqrex  11577  sqrtdiv  11593  absvalsq  11604  absreimsq  11618  absdivap  11621  cau3lem  11665  maxabslemlub  11758  maxabslemval  11759  max0addsup  11770  minabs  11787  bdtrilem  11790  bdtri  11791  xrmaxaddlem  11811  xrmaxadd  11812  xrbdtri  11827  clim  11832  clim2  11834  climshftlemg  11853  climshft2  11857  climcn1  11859  climcn2  11860  subcn2  11862  reccn2ap  11864  climmulc2  11882  climsubc2  11884  clim2ser  11888  iser3shft  11897  climcau  11898  serf0  11903  fzosump1  11968  fsum1p  11969  fsump1  11971  sumsplitdc  11983  fsump1i  11984  mptfzshft  11993  fisum0diag2  11998  fsumconst  12005  fsumdifsnconst  12006  modfsummodlemstep  12008  modfsummod  12009  telfsumo  12017  fsumparts  12021  fsumrelem  12022  hash2iun1dif1  12031  binomlem  12034  binom  12035  binom1p  12036  binom1dif  12038  bcxmas  12040  isumsplit  12042  isum1p  12043  arisum  12049  arisum2  12050  trireciplem  12051  geoserap  12058  geolim  12062  geolim2  12063  georeclim  12064  geo2sum  12065  geoisum1  12070  cvgratnnlemseq  12077  cvgratnnlemsumlt  12079  cvgratnnlemfm  12080  cvgratz  12083  mertenslemi1  12086  mertenslem2  12087  mertensabs  12088  fprod1p  12150  fprodp1  12151  fprodcl2lem  12156  fprodfac  12166  fprodeq0  12168  fprodconst  12171  fprodrec  12180  fprodsplit1f  12185  fprodmodd  12192  efcllemp  12209  ef0lem  12211  efval  12212  esum  12213  ege2le3  12222  efaddlem  12225  efsep  12242  effsumlt  12243  eft0val  12244  efgt1p2  12246  efgt1p  12247  sinval  12253  cosval  12254  resinval  12266  recosval  12267  efi4p  12268  resin4p  12269  recos4p  12270  sinneg  12277  cosneg  12278  efival  12283  sinadd  12287  cosadd  12288  tanaddap  12290  sinmul  12295  cosmul  12296  cos2t  12301  cos2tsin  12302  ef01bndlem  12307  absefib  12322  demoivre  12324  demoivreALT  12325  eirraplem  12328  p1modz1  12345  dvdsmodexp  12346  moddvds  12350  mulmoddvds  12414  3dvds2dec  12417  zeo3  12419  odd2np1lem  12423  odd2np1  12424  oexpneg  12428  2tp1odd  12435  ltoddhalfle  12444  opoe  12446  opeo  12448  omeo  12449  m1expo  12451  m1exp1  12452  nn0o1gt2  12456  nn0o  12458  divalglemnn  12469  divalglemqt  12470  divalglemeunn  12472  divalglemex  12473  divalglemeuneg  12474  flodddiv4  12487  flodddiv4t2lthalf  12490  bitsp1o  12504  bitsmod  12507  bitsinv1lem  12512  gcdaddm  12545  bezoutlemnewy  12557  bezoutlema  12560  bezoutlemb  12561  bezoutlemex  12562  bezoutlemaz  12564  mulgcd  12577  gcddiv  12580  gcdmultiplez  12582  rpmulgcd  12587  rplpwr  12588  uzwodc  12598  lcmgcdlem  12639  lcmgcd  12640  divgcdcoprmex  12664  cncongr2  12666  prmexpb  12713  rpexp  12715  rpexp1i  12716  sqrt2irrlem  12723  oddpwdclemxy  12731  oddpwdclemndvds  12733  sqpweven  12737  2sqpwodd  12738  sqne2sq  12739  qmuldeneqnum  12757  nn0gcdsq  12762  zgcdsq  12763  numdensq  12764  dfphi2  12782  phiprmpw  12784  phiprm  12785  eulerthlema  12792  eulerthlemh  12793  eulerthlemth  12794  fermltl  12796  prmdiv  12797  prmdiveq  12798  prmdivdiv  12799  hashgcdlem  12800  odzval  12804  odzcllem  12805  odzdvds  12808  vfermltl  12814  powm2modprm  12815  reumodprminv  12816  modprm0  12817  nnnn0modprm0  12818  modprmn0modprm0  12819  coprimeprodsq  12820  coprimeprodsq2  12821  pythagtriplem1  12828  pythagtriplem3  12830  pythagtriplem4  12831  pythagtriplem6  12833  pythagtriplem7  12834  pythagtriplem12  12838  pythagtriplem14  12840  pythagtriplem15  12841  pythagtriplem16  12842  pythagtriplem17  12843  pythagtriplem18  12844  pceu  12858  pczpre  12860  pcdiv  12865  pcqdiv  12870  pcrec  12871  pczndvds  12879  pcneg  12888  pc2dvds  12893  pcprmpw2  12896  pcaddlem  12902  pcadd  12903  fldivp1  12911  pockthlem  12919  pockthi  12921  4sqlem5  12945  4sqlem9  12949  4sqlem10  12950  4sqlem2  12952  4sqlem3  12953  4sqlem4  12955  mul4sqlem  12956  4sqlem11  12964  4sqlem12  12965  4sqlem14  12967  4sqlem15  12968  4sqlem17  12970  4sqlem19  12972  ennnfonelemkh  13023  ennnfonelemhf1o  13024  setscomd  13113  ressressg  13148  qusex  13398  qusin  13399  grpinvalem  13458  grpinva  13459  grprida  13460  gsumsplit1r  13471  isnsgrp  13479  sgrpass  13481  sgrp1  13484  sgrppropd  13486  prdssgrpd  13488  mnd12g  13501  mndpropd  13513  prdsidlem  13520  prdsmndd  13521  imasmnd2  13525  mhmex  13535  mhmlin  13540  grprcan  13610  grpinvid1  13625  isgrpinv  13627  grplcan  13635  grpasscan1  13636  grplmulf1o  13647  grpinvadd  13651  grpinvsub  13655  grpsubsub4  13666  grppnpcan2  13667  grpnpncan  13668  dfgrp3mlem  13671  dfgrp3m  13672  grplactcnv  13675  prdsinvlem  13681  imasgrp2  13687  mhmlem  13691  mhmid  13692  mhmmnd  13693  mulgnnp1  13707  mulg2  13708  mulgnn0p1  13710  mulgsubcl  13713  mulgneg  13717  mulgaddcomlem  13722  mulgaddcom  13723  mulgz  13727  mulgnn0dir  13729  mulgdirlem  13730  mulgdir  13731  mulgneg2  13733  mulgnnass  13734  mulgnn0ass  13735  mulgass  13736  mulgassr  13737  mulgmodid  13738  mulgsubdir  13739  submmulg  13743  isnsg3  13784  nmzsubg  13787  ssnmz  13788  0nsg  13791  eqger  13801  eqgid  13803  eqgcpbl  13805  ghmlin  13825  ghmmulg  13833  ghmnsgima  13845  ghmnsgpreima  13846  conjghm  13853  conjnmz  13856  ablsub2inv  13888  abladdsub4  13891  abladdsub  13892  ablpncan2  13893  ablpnpcan  13897  ablnncan  13898  ablnnncan1  13901  gsumfzconst  13918  gsumfzsnfd  13922  mgpress  13934  rngass  13942  rngdi  13943  rngdir  13944  rnglz  13948  rngmneg1  13950  rngsubdir  13955  rngpropd  13958  imasrng  13959  srgass  13974  srgmulgass  13992  srgpcomp  13993  srgpcompp  13994  srgpcomppsc  13995  ringpropd  14041  ringlz  14046  ring1eq0  14051  ringnegl  14054  ringmneg1  14056  ringsubdir  14060  mulgass2  14061  ring1  14062  imasring  14067  opprrng  14080  opprring  14082  unitgrp  14120  dvrcan1  14144  rdivmuldivd  14148  subrginv  14241  resrhm  14252  unitrrg  14271  islmod  14295  lmodlema  14296  islmodd  14297  lmod0vs  14325  lmodvs0  14326  lmodvsmmulgdi  14327  lmodvneg1  14334  lmodvsneg  14335  lmodsubvs  14347  lmodsubdi  14348  lmodsubdir  14349  lmodprop2d  14352  rmodislmodlem  14354  rmodislmod  14355  lsssetm  14360  islssmd  14363  lssclg  14368  lssvacl  14369  lss1d  14387  lsspropdg  14435  sraval  14441  rnglidlmcl  14484  gsumfzfsumlemm  14591  znunit  14663  mplsubgfilemcl  14703  resttop  14884  restco  14888  restin  14890  lmfval  14907  cnprcl2k  14920  txrest  14990  txdis1cn  14992  cnmpt2res  15011  psmettri2  15042  psmettri  15044  xmettri2  15075  xmettri  15086  mettri  15087  metrtri  15091  blvalps  15102  blval  15103  xblss2  15119  blhalf  15122  comet  15213  xmetxp  15221  txmetcnp  15232  cnmet  15244  ioo2bl  15265  ivthreinc  15359  limcmpted  15377  limcimolemlt  15378  cnplimclemr  15383  limccnp2cntop  15391  reldvg  15393  dvfvalap  15395  dvidlemap  15405  dvidrelem  15406  dvidsslem  15407  dvconst  15408  dvconstre  15410  dvconstss  15412  dvcnp2cntop  15413  dvaddxxbr  15415  dvmulxxbr  15416  dvcoapbr  15421  dvcjbr  15422  dvexp  15425  dvrecap  15427  dvmptcmulcn  15435  dveflem  15440  plyval  15446  elply2  15449  elplyr  15454  elplyd  15455  ply1termlem  15456  plyaddlem1  15461  plymullem1  15462  plycoeid3  15471  plycjlemc  15474  dvply1  15479  sin0pilem1  15495  sinperlem  15522  ptolemy  15538  tangtx  15552  abssinper  15560  reexplog  15585  relogexp  15586  cxprec  15624  rpdivcxp  15625  cxpmul  15626  rpabscxpbnd  15654  rplogbval  15659  rplogbreexp  15667  rprelogbmul  15669  logbrec  15674  logbgcd1irraplemap  15683  binom4  15693  wilthlem1  15694  mpodvdsmulf1o  15704  sgmppw  15706  0sgmppw  15707  1sgmprm  15708  1sgm2ppw  15709  perfectlem1  15713  perfectlem2  15714  perfect  15715  lgslem1  15719  lgslem4  15722  lgsval  15723  lgsfvalg  15724  lgsval2lem  15729  lgsval4lem  15730  lgsvalmod  15738  lgsneg  15743  lgsneg1  15744  lgsmod  15745  lgsdilem  15746  lgsdir2lem4  15750  lgsdir2  15752  lgsdirprm  15753  lgsdir  15754  lgsne0  15757  lgssq  15759  lgssq2  15760  lgsmulsqcoprm  15765  lgsdirnn0  15766  lgsdinn0  15767  gausslemma2dlem1a  15777  gausslemma2dlem4  15783  gausslemma2dlem5a  15784  gausslemma2dlem5  15785  gausslemma2dlem6  15786  gausslemma2dlem7  15787  gausslemma2d  15788  lgseisenlem1  15789  lgseisenlem2  15790  lgseisenlem3  15791  lgseisenlem4  15792  lgseisen  15793  lgsquadlem1  15796  lgsquadlem2  15797  lgsquad2lem1  15800  lgsquad2lem2  15801  lgsquad3  15803  m1lgs  15804  2lgslem1a  15807  2lgslem1c  15809  2lgslem3a  15812  2lgslem3b  15813  2lgslem3c  15814  2lgslem3d  15815  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  2lgsoddprmlem1  15824  2lgsoddprmlem2  15825  2lgsoddprmlem3  15830  2sqlem1  15833  2sqlem2  15834  mul2sq  15835  2sqlem3  15836  2sqlem4  15837  2sqlem8  15842  2sqlem9  15843  2sqlem10  15844  uspgr2wlkeqi  16164  isclwwlk  16189  clwwlkccatlem  16195  clwwlknonex2  16234  trilpolemeq1  16580  trilpolemlt1  16581  trirec0xor  16585  apdifflemf  16586  apdiff  16588