Theorem oveq1d 6043

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

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

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 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-rex 2517  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-iota 5293  df-fv 5341  df-ov 6031

This theorem is referenced by:  fvoveq1d  6050  csbov2g  6070  caovassg  6191  caovdig  6207  caovdirg  6210  caov12d  6214  caov31d  6215  caov411d  6218  caofinvl  6270  suppofss1dcl  6442  suppofss2dcl  6443  omsuc  6683  nnmsucr  6699  nnm1  6736  nnm2  6737  ecovass  6856  ecoviass  6857  ecovdi  6858  ecovidi  6859  isacnm  7461  addasspig  7593  mulasspig  7595  mulpipq2  7634  distrnqg  7650  ltsonq  7661  ltanqg  7663  ltmnqg  7664  ltexnqq  7671  archnqq  7680  prarloclemarch2  7682  enq0sym  7695  addnq0mo  7710  mulnq0mo  7711  addnnnq0  7712  nqpnq0nq  7716  nq0m0r  7719  nq0a0  7720  nnanq0  7721  distrnq0  7722  addassnq0  7725  addpinq1  7727  prarloclemlo  7757  prarloclem3  7760  prarloclem5  7763  prarloclemcalc  7765  addnqprllem  7790  addnqprulem  7791  appdivnq  7826  recexprlem1ssl  7896  recexprlem1ssu  7897  ltmprr  7905  cauappcvgprlemladdru  7919  cauappcvgprlem1  7922  caucvgprlemnkj  7929  caucvgprlemnbj  7930  caucvgprlemcl  7939  caucvgprlemladdfu  7940  caucvgprlemladdrl  7941  caucvgprlem1  7942  caucvgprprlemcbv  7950  caucvgprprlemval  7951  caucvgprprlemexb  7970  caucvgprprlem1  7972  addcmpblnr  8002  mulcmpblnrlemg  8003  addsrmo  8006  mulsrmo  8007  addsrpr  8008  mulsrpr  8009  ltsrprg  8010  1idsr  8031  pn0sr  8034  recexgt0sr  8036  mulgt0sr  8041  srpospr  8046  prsradd  8049  caucvgsrlemfv  8054  caucvgsrlemcau  8056  caucvgsrlemgt1  8058  caucvgsrlemoffval  8059  caucvgsrlemoffcau  8061  caucvgsrlemoffres  8063  caucvgsrlembnd  8064  caucvgsr  8065  map2psrprg  8068  pitonnlem1p1  8109  pitonnlem2  8110  pitonn  8111  recidpirqlemcalc  8120  ax1rid  8140  axrnegex  8142  axcnre  8144  recriota  8153  nntopi  8157  axcaucvglemval  8160  axcaucvglemcau  8161  axcaucvglemres  8162  mul12  8350  mul4  8353  muladd11  8354  readdcan  8361  muladd11r  8377  add12  8379  cnegex  8399  addcan  8401  negeu  8412  pncan2  8428  addsubass  8431  addsub  8432  2addsub  8435  addsubeq4  8436  subid  8440  subid1  8441  npncan  8442  nppcan  8443  nnpcan  8444  nnncan1  8457  npncan3  8459  pnpcan  8460  pnncan  8462  ppncan  8463  addsub4  8464  negsub  8469  subneg  8470  subeqxfrd  8584  mvlraddd  8585  mvlladdd  8586  mvrraddd  8587  subaddeqd  8590  ine0  8615  mulneg1  8616  ltadd2  8641  apreap  8809  cru  8824  recexap  8875  mulcanapd  8883  div23ap  8913  div13ap  8915  divmulassap  8917  divmulasscomap  8918  divcanap4  8921  muldivdirap  8929  divsubdirap  8930  divmuldivap  8934  divdivdivap  8935  divcanap5  8936  divmul13ap  8937  divmuleqap  8939  divdiv32ap  8942  divcanap7  8943  dmdcanap  8944  divdivap1  8945  divdivap2  8946  divadddivap  8949  divsubdivap  8950  conjmulap  8951  divneg2ap  8958  subrecap  9061  mvllmulapd  9064  lt2mul2div  9101  nndivtr  9227  2halves  9415  halfaddsub  9420  subhalfhalf  9421  avgle1  9427  avgle2  9428  div4p1lem1div2  9440  un0addcl  9477  un0mulcl  9478  peano2z  9559  zneo  9625  nneoor  9626  nneo  9627  zeo  9629  zeo2  9630  deceq1  9659  qreccl  9920  xaddcom  10140  xnegdi  10147  xaddass  10148  xaddass2  10149  xpncan  10150  xleadd1a  10152  xltadd1  10155  xposdif  10161  xadd4d  10164  lincmb01cmp  10282  lincmble  10283  iccf1o  10284  fz0to4untppr  10404  fzo0addel  10479  fzosubel3  10487  qavgle  10564  2tnp1ge0ge0  10607  fldiv4p1lem1div2  10611  fldiv4lem1div2  10613  ceilqm1lt  10620  flqdiv  10629  modqlt  10641  modqdiffl  10643  modqcyc2  10668  modqaddabs  10670  mulqaddmodid  10672  mulp1mod1  10673  modqmuladd  10674  modqmuladdnn0  10676  qnegmod  10677  addmodid  10680  addmodidr  10681  modqadd2mod  10682  modqm1p1mod0  10683  modqmul12d  10686  modqnegd  10687  modqadd12d  10688  modqsub12d  10689  q2submod  10693  modqmulmodr  10698  modqaddmulmod  10699  modqsubdir  10701  modfzo0difsn  10703  modsumfzodifsn  10704  addmodlteq  10706  frecuzrdgsuc  10722  frecfzennn  10734  iseqovex  10766  seq3-1p  10798  seq3caopr2  10801  seqcaopr2g  10802  seq3caopr  10803  seqcaoprg  10804  seqf1oglem2a  10826  seqf1oglem1  10827  seqf1oglem2  10828  seq3id  10833  seq3homo  10835  seq3z  10836  seqhomog  10838  seqfeq4g  10839  expp1  10854  exprecap  10888  expaddzaplem  10890  expmulzap  10893  expdivap  10898  sqval  10905  sqsubswap  10907  sqdividap  10912  subsq  10954  subsq2  10955  binom2  10959  binom2sub  10961  mulbinom2  10964  binom3  10965  zesq  10966  bernneq2  10969  modqexp  10974  sqoddm1div8  11001  mulsubdivbinom2ap  11019  nn0opthlem1d  11028  nn0opthd  11030  nn0opth2d  11031  facp1  11038  facdiv  11046  facndiv  11047  faclbnd  11049  faclbnd2  11050  faclbnd3  11051  bcval  11057  bccmpl  11062  bcm1k  11068  bcp1n  11069  bcp1nk  11070  bcval5  11071  bcp1m1  11073  bcpasc  11074  bcn2m1  11077  hashprg  11118  hashdifpr  11130  hashfzo  11132  hashfzp1  11134  hashfz0  11135  hashxp  11136  zfz1isolemsplit  11148  zfz1isolem1  11150  seq3coll  11152  lswwrd  11209  ccatfvalfi  11218  ccatass  11234  lswccatn0lsw  11237  wrdlenccats1lenm1g  11262  ccatw2s1leng  11264  ccatswrd  11300  ccatpfx  11331  swrdpfx  11337  pfxpfx  11338  ccats1pfxeq  11344  wrdeqs1cat  11350  wrdind  11352  wrd2ind  11353  pfxccatpfx2  11367  pfxccatin12d  11375  cats1catd  11398  cats2catd  11399  s2leng  11419  s3s4d  11433  s2s5d  11434  s5s2d  11435  reval  11472  crre  11480  remim  11483  remul2  11496  immul2  11503  imval2  11517  cjdivap  11532  caucvgre  11604  cvg1nlemcau  11607  cvg1nlemres  11608  resqrexlemp1rp  11629  resqrexlemfp1  11632  resqrexlemover  11633  resqrexlemcalc1  11637  resqrexlemcalc3  11639  resqrexlemnm  11641  resqrexlemoverl  11644  resqrexlemglsq  11645  resqrexlemga  11646  resqrexlemsqa  11647  resqrexlemex  11648  resqrex  11649  sqrtdiv  11665  absvalsq  11676  absreimsq  11690  absdivap  11693  cau3lem  11737  maxabslemlub  11830  maxabslemval  11831  max0addsup  11842  minabs  11859  bdtrilem  11862  bdtri  11863  xrmaxaddlem  11883  xrmaxadd  11884  xrbdtri  11899  clim  11904  clim2  11906  climshftlemg  11925  climshft2  11929  climcn1  11931  climcn2  11932  subcn2  11934  reccn2ap  11936  climmulc2  11954  climsubc2  11956  clim2ser  11960  iser3shft  11969  climcau  11970  serf0  11975  fzosump1  12041  fsum1p  12042  fsump1  12044  sumsplitdc  12056  fsump1i  12057  mptfzshft  12066  fisum0diag2  12071  fsumconst  12078  fsumdifsnconst  12079  modfsummodlemstep  12081  modfsummod  12082  telfsumo  12090  fsumparts  12094  fsumrelem  12095  hash2iun1dif1  12104  binomlem  12107  binom  12108  binom1p  12109  binom1dif  12111  bcxmas  12113  isumsplit  12115  isum1p  12116  arisum  12122  arisum2  12123  trireciplem  12124  geoserap  12131  geolim  12135  geolim2  12136  georeclim  12137  geo2sum  12138  geoisum1  12143  cvgratnnlemseq  12150  cvgratnnlemsumlt  12152  cvgratnnlemfm  12153  cvgratz  12156  mertenslemi1  12159  mertenslem2  12160  mertensabs  12161  fprod1p  12223  fprodp1  12224  fprodcl2lem  12229  fprodfac  12239  fprodeq0  12241  fprodconst  12244  fprodrec  12253  fprodsplit1f  12258  fprodmodd  12265  efcllemp  12282  ef0lem  12284  efval  12285  esum  12286  ege2le3  12295  efaddlem  12298  efsep  12315  effsumlt  12316  eft0val  12317  efgt1p2  12319  efgt1p  12320  sinval  12326  cosval  12327  resinval  12339  recosval  12340  efi4p  12341  resin4p  12342  recos4p  12343  sinneg  12350  cosneg  12351  efival  12356  sinadd  12360  cosadd  12361  tanaddap  12363  sinmul  12368  cosmul  12369  cos2t  12374  cos2tsin  12375  ef01bndlem  12380  absefib  12395  demoivre  12397  demoivreALT  12398  eirraplem  12401  p1modz1  12418  dvdsmodexp  12419  moddvds  12423  mulmoddvds  12487  3dvds2dec  12490  zeo3  12492  odd2np1lem  12496  odd2np1  12497  oexpneg  12501  2tp1odd  12508  ltoddhalfle  12517  opoe  12519  opeo  12521  omeo  12522  m1expo  12524  m1exp1  12525  nn0o1gt2  12529  nn0o  12531  divalglemnn  12542  divalglemqt  12543  divalglemeunn  12545  divalglemex  12546  divalglemeuneg  12547  flodddiv4  12560  flodddiv4t2lthalf  12563  bitsp1o  12577  bitsmod  12580  bitsinv1lem  12585  gcdaddm  12618  bezoutlemnewy  12630  bezoutlema  12633  bezoutlemb  12634  bezoutlemex  12635  bezoutlemaz  12637  mulgcd  12650  gcddiv  12653  gcdmultiplez  12655  rpmulgcd  12660  rplpwr  12661  uzwodc  12671  lcmgcdlem  12712  lcmgcd  12713  divgcdcoprmex  12737  cncongr2  12739  prmexpb  12786  rpexp  12788  rpexp1i  12789  sqrt2irrlem  12796  oddpwdclemxy  12804  oddpwdclemndvds  12806  sqpweven  12810  2sqpwodd  12811  sqne2sq  12812  qmuldeneqnum  12830  nn0gcdsq  12835  zgcdsq  12836  numdensq  12837  dfphi2  12855  phiprmpw  12857  phiprm  12858  eulerthlema  12865  eulerthlemh  12866  eulerthlemth  12867  fermltl  12869  prmdiv  12870  prmdiveq  12871  prmdivdiv  12872  hashgcdlem  12873  odzval  12877  odzcllem  12878  odzdvds  12881  vfermltl  12887  powm2modprm  12888  reumodprminv  12889  modprm0  12890  nnnn0modprm0  12891  modprmn0modprm0  12892  coprimeprodsq  12893  coprimeprodsq2  12894  pythagtriplem1  12901  pythagtriplem3  12903  pythagtriplem4  12904  pythagtriplem6  12906  pythagtriplem7  12907  pythagtriplem12  12911  pythagtriplem14  12913  pythagtriplem15  12914  pythagtriplem16  12915  pythagtriplem17  12916  pythagtriplem18  12917  pceu  12931  pczpre  12933  pcdiv  12938  pcqdiv  12943  pcrec  12944  pczndvds  12952  pcneg  12961  pc2dvds  12966  pcprmpw2  12969  pcaddlem  12975  pcadd  12976  fldivp1  12984  pockthlem  12992  pockthi  12994  4sqlem5  13018  4sqlem9  13022  4sqlem10  13023  4sqlem2  13025  4sqlem3  13026  4sqlem4  13028  mul4sqlem  13029  4sqlem11  13037  4sqlem12  13038  4sqlem14  13040  4sqlem15  13041  4sqlem17  13043  4sqlem19  13045  ennnfonelemkh  13096  ennnfonelemhf1o  13097  setscomd  13186  ressressg  13221  qusex  13471  qusin  13472  grpinvalem  13531  grpinva  13532  grprida  13533  gsumsplit1r  13544  isnsgrp  13552  sgrpass  13554  sgrp1  13557  sgrppropd  13559  prdssgrpd  13561  mnd12g  13574  mndpropd  13586  prdsidlem  13593  prdsmndd  13594  imasmnd2  13598  mhmex  13608  mhmlin  13613  grprcan  13683  grpinvid1  13698  isgrpinv  13700  grplcan  13708  grpasscan1  13709  grplmulf1o  13720  grpinvadd  13724  grpinvsub  13728  grpsubsub4  13739  grppnpcan2  13740  grpnpncan  13741  dfgrp3mlem  13744  dfgrp3m  13745  grplactcnv  13748  prdsinvlem  13754  imasgrp2  13760  mhmlem  13764  mhmid  13765  mhmmnd  13766  mulgnnp1  13780  mulg2  13781  mulgnn0p1  13783  mulgsubcl  13786  mulgneg  13790  mulgaddcomlem  13795  mulgaddcom  13796  mulgz  13800  mulgnn0dir  13802  mulgdirlem  13803  mulgdir  13804  mulgneg2  13806  mulgnnass  13807  mulgnn0ass  13808  mulgass  13809  mulgassr  13810  mulgmodid  13811  mulgsubdir  13812  submmulg  13816  isnsg3  13857  nmzsubg  13860  ssnmz  13861  0nsg  13864  eqger  13874  eqgid  13876  eqgcpbl  13878  ghmlin  13898  ghmmulg  13906  ghmnsgima  13918  ghmnsgpreima  13919  conjghm  13926  conjnmz  13929  ablsub2inv  13961  abladdsub4  13964  abladdsub  13965  ablpncan2  13966  ablpnpcan  13970  ablnncan  13971  ablnnncan1  13974  gsumfzconst  13991  gsumfzsnfd  13995  gsumsplit0  13996  mgpress  14008  rngass  14016  rngdi  14017  rngdir  14018  rnglz  14022  rngmneg1  14024  rngsubdir  14029  rngpropd  14032  imasrng  14033  srgass  14048  srgmulgass  14066  srgpcomp  14067  srgpcompp  14068  srgpcomppsc  14069  ringpropd  14115  ringlz  14120  ring1eq0  14125  ringnegl  14128  ringmneg1  14130  ringsubdir  14134  mulgass2  14135  ring1  14136  imasring  14141  opprrng  14154  opprring  14156  unitgrp  14194  dvrcan1  14218  rdivmuldivd  14222  subrginv  14315  resrhm  14326  unitrrg  14346  islmod  14370  lmodlema  14371  islmodd  14372  lmod0vs  14400  lmodvs0  14401  lmodvsmmulgdi  14402  lmodvneg1  14409  lmodvsneg  14410  lmodsubvs  14422  lmodsubdi  14423  lmodsubdir  14424  lmodprop2d  14427  rmodislmodlem  14429  rmodislmod  14430  lsssetm  14435  islssmd  14438  lssclg  14443  lssvacl  14444  lss1d  14462  lsspropdg  14510  sraval  14516  rnglidlmcl  14559  gsumfzfsumlemm  14666  znunit  14738  mplsubgfilemcl  14783  resttop  14964  restco  14968  restin  14970  lmfval  14987  cnprcl2k  15000  txrest  15070  txdis1cn  15072  cnmpt2res  15091  psmettri2  15122  psmettri  15124  xmettri2  15155  xmettri  15166  mettri  15167  metrtri  15171  blvalps  15182  blval  15183  xblss2  15199  blhalf  15202  comet  15293  xmetxp  15301  txmetcnp  15312  cnmet  15324  ioo2bl  15345  ivthreinc  15439  limcmpted  15457  limcimolemlt  15458  cnplimclemr  15463  limccnp2cntop  15471  reldvg  15473  dvfvalap  15475  dvidlemap  15485  dvidrelem  15486  dvidsslem  15487  dvconst  15488  dvconstre  15490  dvconstss  15492  dvcnp2cntop  15493  dvaddxxbr  15495  dvmulxxbr  15496  dvcoapbr  15501  dvcjbr  15502  dvexp  15505  dvrecap  15507  dvmptcmulcn  15515  dveflem  15520  plyval  15526  elply2  15529  elplyr  15534  elplyd  15535  ply1termlem  15536  plyaddlem1  15541  plymullem1  15542  plycoeid3  15551  plycjlemc  15554  dvply1  15559  sin0pilem1  15575  sinperlem  15602  ptolemy  15618  tangtx  15632  abssinper  15640  reexplog  15665  relogexp  15666  cxprec  15704  rpdivcxp  15705  cxpmul  15706  rpabscxpbnd  15734  rplogbval  15739  rplogbreexp  15747  rprelogbmul  15749  logbrec  15754  logbgcd1irraplemap  15763  binom4  15773  pellexlem2  15775  pellexlem3  15776  wilthlem1  15777  mpodvdsmulf1o  15787  sgmppw  15789  0sgmppw  15790  1sgmprm  15791  1sgm2ppw  15792  perfectlem1  15796  perfectlem2  15797  perfect  15798  lgslem1  15802  lgslem4  15805  lgsval  15806  lgsfvalg  15807  lgsval2lem  15812  lgsval4lem  15813  lgsvalmod  15821  lgsneg  15826  lgsneg1  15827  lgsmod  15828  lgsdilem  15829  lgsdir2lem4  15833  lgsdir2  15835  lgsdirprm  15836  lgsdir  15837  lgsne0  15840  lgssq  15842  lgssq2  15843  lgsmulsqcoprm  15848  lgsdirnn0  15849  lgsdinn0  15850  gausslemma2dlem1a  15860  gausslemma2dlem4  15866  gausslemma2dlem5a  15867  gausslemma2dlem5  15868  gausslemma2dlem6  15869  gausslemma2dlem7  15870  gausslemma2d  15871  lgseisenlem1  15872  lgseisenlem2  15873  lgseisenlem3  15874  lgseisenlem4  15875  lgseisen  15876  lgsquadlem1  15879  lgsquadlem2  15880  lgsquad2lem1  15883  lgsquad2lem2  15884  lgsquad3  15886  m1lgs  15887  2lgslem1a  15890  2lgslem1c  15892  2lgslem3a  15895  2lgslem3b  15896  2lgslem3c  15897  2lgslem3d  15898  2lgslem3a1  15899  2lgslem3b1  15900  2lgslem3c1  15901  2lgslem3d1  15902  2lgsoddprmlem1  15907  2lgsoddprmlem2  15908  2lgsoddprmlem3  15913  2sqlem1  15916  2sqlem2  15917  mul2sq  15918  2sqlem3  15919  2sqlem4  15920  2sqlem8  15925  2sqlem9  15926  2sqlem10  15927  vdegp1bid  16239  uspgr2wlkeqi  16291  isclwwlk  16318  clwwlkccatlem  16324  clwwlknonex2  16363  repiecele0  16741  repiecege0  16742  repiecef  16743  trilpolemeq1  16755  trilpolemlt1  16756  trirec0xor  16760  apdifflemf  16761  apdiff  16763  qdiff  16764  gsumgfsumlem  16795  gsumgfsum  16796