Theorem oveq1d 6090

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

Syntax hints:   → wi 4   = wceq 1402  (class class class)co 6075

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-rex 2534  df-v 2823  df-un 3224  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-br 4126  df-iota 5332  df-fv 5380  df-ov 6078

This theorem is referenced by:  fvoveq1d  6097  csbov2g  6117  caovassg  6238  caovdig  6254  caovdirg  6257  caov12d  6261  caov31d  6262  caov411d  6265  caofinvl  6318  suppofss1dcl  6494  suppofss2dcl  6495  omsuc  6735  nnmsucr  6751  nnm1  6788  nnm2  6789  ecovass  6908  ecoviass  6909  ecovdi  6910  ecovidi  6911  isacnm  7549  addasspig  7687  mulasspig  7689  mulpipq2  7728  distrnqg  7744  ltsonq  7755  ltanqg  7757  ltmnqg  7758  ltexnqq  7765  archnqq  7774  prarloclemarch2  7776  enq0sym  7789  addnq0mo  7804  mulnq0mo  7805  addnnnq0  7806  nqpnq0nq  7810  nq0m0r  7813  nq0a0  7814  nnanq0  7815  distrnq0  7816  addassnq0  7819  addpinq1  7821  prarloclemlo  7851  prarloclem3  7854  prarloclem5  7857  prarloclemcalc  7859  addnqprllem  7884  addnqprulem  7885  appdivnq  7920  recexprlem1ssl  7990  recexprlem1ssu  7991  ltmprr  7999  cauappcvgprlemladdru  8013  cauappcvgprlem1  8016  caucvgprlemnkj  8023  caucvgprlemnbj  8024  caucvgprlemcl  8033  caucvgprlemladdfu  8034  caucvgprlemladdrl  8035  caucvgprlem1  8036  caucvgprprlemcbv  8044  caucvgprprlemval  8045  caucvgprprlemexb  8064  caucvgprprlem1  8066  addcmpblnr  8096  mulcmpblnrlemg  8097  addsrmo  8100  mulsrmo  8101  addsrpr  8102  mulsrpr  8103  ltsrprg  8104  1idsr  8125  pn0sr  8128  recexgt0sr  8130  mulgt0sr  8135  srpospr  8140  prsradd  8143  caucvgsrlemfv  8148  caucvgsrlemcau  8150  caucvgsrlemgt1  8152  caucvgsrlemoffval  8153  caucvgsrlemoffcau  8155  caucvgsrlemoffres  8157  caucvgsrlembnd  8158  caucvgsr  8159  map2psrprg  8162  pitonnlem1p1  8203  pitonnlem2  8204  pitonn  8205  recidpirqlemcalc  8214  ax1rid  8234  axrnegex  8236  axcnre  8238  recriota  8247  nntopi  8251  axcaucvglemval  8254  axcaucvglemcau  8255  axcaucvglemres  8256  mul12  8445  mul4  8448  muladd11  8449  readdcan  8456  muladd11r  8472  add12  8474  cnegex  8494  addcan  8496  negeu  8507  pncan2  8523  addsubass  8526  addsub  8527  2addsub  8530  addsubeq4  8531  subid  8535  subid1  8536  npncan  8537  nppcan  8538  nnpcan  8539  nnncan1  8552  npncan3  8554  pnpcan  8555  pnncan  8557  ppncan  8558  addsub4  8559  negsub  8564  subneg  8565  subeqxfrd  8679  mvlraddd  8680  mvlladdd  8681  mvrraddd  8682  subaddeqd  8685  ine0  8711  mulneg1  8712  ltadd2  8737  apreap  8905  cru  8920  recexap  8971  mulcanapd  8979  div23ap  9011  div13ap  9013  divmulassap  9015  divmulasscomap  9016  divcanap4  9019  muldivdirap  9027  divsubdirap  9028  divmuldivap  9032  divdivdivap  9033  divcanap5  9034  divmul13ap  9035  divmuleqap  9037  divdiv32ap  9040  divcanap7  9041  dmdcanap  9042  divdivap1  9043  divdivap2  9044  divadddivap  9047  divsubdivap  9048  conjmulap  9049  divneg2ap  9056  subrecap  9159  mvllmulapd  9162  lt2mul2div  9199  nndivtr  9325  2halves  9513  halfaddsub  9518  subhalfhalf  9519  avgle1  9525  avgle2  9526  div4p1lem1div2  9538  un0addcl  9575  un0mulcl  9576  peano2z  9659  zneo  9726  nneoor  9727  nneo  9728  zeo  9730  zeo2  9731  deceq1  9760  qreccl  10021  xaddcom  10242  xnegdi  10249  xaddass  10250  xaddass2  10251  xpncan  10252  xleadd1a  10254  xltadd1  10257  xposdif  10263  xadd4d  10266  lincmb01cmp  10384  lincmble  10385  iccf1o  10386  fzspl  10454  fz0to4untppr  10509  fzo0addel  10584  fzosubel3  10592  qavgle  10671  2tnp1ge0ge0  10714  fldiv4p1lem1div2  10718  fldiv4lem1div2  10720  ceilqm1lt  10727  flqdiv  10736  modqlt  10748  modqdiffl  10750  modqcyc2  10775  modqaddabs  10777  mulqaddmodid  10779  mulp1mod1  10780  modqmuladd  10781  modqmuladdnn0  10783  qnegmod  10784  addmodid  10787  addmodidr  10788  modqadd2mod  10789  modqm1p1mod0  10790  modqmul12d  10793  modqnegd  10794  modqadd12d  10795  modqsub12d  10796  q2submod  10800  modqmulmodr  10805  modqaddmulmod  10806  modqsubdir  10808  modfzo0difsn  10810  modsumfzodifsn  10811  addmodlteq  10813  frecuzrdgsuc  10829  frecfzennn  10841  iseqovex  10873  seq3-1p  10905  seq3caopr2  10908  seqcaopr2g  10909  seq3caopr  10910  seqcaoprg  10911  seqf1oglem2a  10933  seqf1oglem1  10934  seqf1oglem2  10935  seq3id  10940  seq3homo  10942  seq3z  10943  seqhomog  10945  seqfeq4g  10946  expp1  10961  exprecap  10995  expaddzaplem  10997  expmulzap  11000  expdivap  11005  sqval  11012  sqsubswap  11014  sqdividap  11019  subsq  11061  subsq2  11062  binom2  11066  binom2sub  11068  mulbinom2  11071  binom3  11072  zesq  11074  bernneq2  11077  modqexp  11082  sqoddm1div8  11109  mulsubdivbinom2ap  11127  nn0opthlem1d  11136  nn0opthd  11138  nn0opth2d  11139  facp1  11146  facdiv  11154  facndiv  11155  faclbnd  11157  faclbnd2  11158  faclbnd3  11159  bcval  11165  bccmpl  11170  bcm1k  11176  bcp1n  11177  bcp1nk  11178  bcval5  11179  bcp1m1  11181  bcpasc  11182  bcm1n  11185  bcn2m1  11186  hashprg  11227  hashdifpr  11239  hashfzo  11241  hashfzp1  11243  hashfz0  11244  hashxp  11245  hashfibclem  11260  hashfibc  11261  hashf1  11265  zfz1isolemsplit  11268  zfz1isolem1  11270  seq3coll  11272  lswwrd  11329  ccatfvalfi  11338  ccatass  11354  lswccatn0lsw  11357  wrdlenccats1lenm1g  11382  ccatw2s1leng  11384  ccatswrd  11420  ccatpfx  11451  swrdpfx  11457  pfxpfx  11458  ccats1pfxeq  11464  wrdeqs1cat  11470  wrdind  11472  wrd2ind  11473  pfxccatpfx2  11487  pfxccatin12d  11495  cats1catd  11518  cats2catd  11519  s2leng  11539  s3s4d  11553  s2s5d  11554  s5s2d  11555  reval  11592  crre  11600  remim  11603  remul2  11616  immul2  11623  imval2  11637  sq01  11638  cjdivap  11653  caucvgre  11725  cvg1nlemcau  11728  cvg1nlemres  11729  resqrexlemp1rp  11750  resqrexlemfp1  11753  resqrexlemover  11754  resqrexlemcalc1  11758  resqrexlemcalc3  11760  resqrexlemnm  11762  resqrexlemoverl  11765  resqrexlemglsq  11766  resqrexlemga  11767  resqrexlemsqa  11768  resqrexlemex  11769  resqrex  11770  sqrtdiv  11786  absvalsq  11797  absreimsq  11811  absdivap  11814  cau3lem  11858  maxabslemlub  11951  maxabslemval  11952  max0addsup  11963  minabs  11980  bdtrilem  11983  bdtri  11984  xrmaxaddlem  12004  xrmaxadd  12005  xrbdtri  12020  clim  12025  clim2  12027  climshftlemg  12046  climshft2  12050  climcn1  12052  climcn2  12053  subcn2  12055  reccn2ap  12057  climmulc2  12075  climsubc2  12077  clim2ser  12081  iser3shft  12090  climcau  12091  serf0  12096  fzosump1  12162  fsum1p  12163  fsump1  12165  sumsplitdc  12177  fsump1i  12178  mptfzshft  12187  fisum0diag2  12192  fsumconst  12199  fsumdifsnconst  12200  modfsummodlemstep  12202  modfsummod  12203  telfsumo  12211  fsumparts  12215  fsumrelem  12216  hash2iun1dif1  12225  binomlem  12228  binom  12229  binom1p  12230  binom1dif  12232  bcxmas  12234  isumsplit  12236  isum1p  12237  arisum  12243  arisum2  12244  trireciplem  12245  geoserap  12252  geolim  12256  geolim2  12257  georeclim  12258  geo2sum  12259  geoisum1  12264  cvgratnnlemseq  12271  cvgratnnlemsumlt  12273  cvgratnnlemfm  12274  cvgratz  12277  mertenslemi1  12280  mertenslem2  12281  mertensabs  12282  fprod1p  12344  fprodp1  12345  fprodcl2lem  12350  fprodfac  12360  fprodeq0  12362  fprodconst  12365  fprodrec  12374  fprodsplit1f  12379  fprodmodd  12386  efcllemp  12403  ef0lem  12405  efval  12406  esum  12407  ege2le3  12416  efaddlem  12419  efsep  12436  effsumlt  12437  eft0val  12438  efgt1p2  12440  efgt1p  12441  sinval  12447  cosval  12448  resinval  12460  recosval  12461  efi4p  12462  resin4p  12463  recos4p  12464  sinneg  12471  cosneg  12472  efival  12477  sinadd  12481  cosadd  12482  tanaddap  12484  sinmul  12489  cosmul  12490  cos2t  12495  cos2tsin  12496  ef01bndlem  12501  absefib  12516  demoivre  12518  demoivreALT  12519  eirraplem  12522  p1modz1  12539  dvdsmodexp  12540  moddvds  12544  mulmoddvds  12608  3dvds2dec  12611  zeo3  12613  odd2np1lem  12617  odd2np1  12618  oexpneg  12622  2tp1odd  12629  ltoddhalfle  12638  opoe  12640  opeo  12642  omeo  12643  m1expo  12645  m1exp1  12646  nn0o1gt2  12650  nn0o  12652  divalglemnn  12663  divalglemqt  12664  divalglemeunn  12666  divalglemex  12667  divalglemeuneg  12668  flodddiv4  12681  flodddiv4t2lthalf  12684  bitsp1o  12698  bitsmod  12701  bitsinv1lem  12706  gcdaddm  12739  bezoutlemnewy  12751  bezoutlema  12754  bezoutlemb  12755  bezoutlemex  12756  bezoutlemaz  12758  mulgcd  12771  gcddiv  12774  gcdmultiplez  12776  rpmulgcd  12781  rplpwr  12782  uzwodc  12792  lcmgcdlem  12833  lcmgcd  12834  divgcdcoprmex  12858  cncongr2  12860  prmexpb  12907  rpexp  12909  rpexp1i  12910  sqrt2irrlem  12917  oddpwdclemxy  12925  oddpwdclemndvds  12927  sqpweven  12931  2sqpwodd  12932  sqne2sq  12933  qmuldeneqnum  12951  nn0gcdsq  12956  zgcdsq  12957  numdensq  12958  dfphi2  12976  phiprmpw  12978  phiprm  12979  eulerthlema  12986  eulerthlemh  12987  eulerthlemth  12988  fermltl  12990  prmdiv  12991  prmdiveq  12992  prmdivdiv  12993  hashgcdlem  12994  odzval  12998  odzcllem  12999  odzdvds  13002  vfermltl  13008  powm2modprm  13009  reumodprminv  13010  modprm0  13011  nnnn0modprm0  13012  modprmn0modprm0  13013  coprimeprodsq  13014  coprimeprodsq2  13015  pythagtriplem1  13022  pythagtriplem3  13024  pythagtriplem4  13025  pythagtriplem6  13027  pythagtriplem7  13028  pythagtriplem12  13032  pythagtriplem14  13034  pythagtriplem15  13035  pythagtriplem16  13036  pythagtriplem17  13037  pythagtriplem18  13038  pceu  13052  pczpre  13054  pcdiv  13059  pcqdiv  13064  pcrec  13065  pczndvds  13073  pcneg  13082  pc2dvds  13087  pcprmpw2  13090  pcaddlem  13096  pcadd  13097  fldivp1  13105  pockthlem  13113  pockthi  13115  4sqlem5  13139  4sqlem9  13143  4sqlem10  13144  4sqlem2  13146  4sqlem3  13147  4sqlem4  13149  mul4sqlem  13150  4sqlem11  13158  4sqlem12  13159  4sqlem14  13161  4sqlem15  13162  4sqlem17  13164  4sqlem19  13166  ballotfilem2  13206  ballotfilemfp1  13209  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilem4  13219  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemsval  13230  ballotfilemsdom  13233  ballotfilemsima  13237  ballotfilemieq  13238  ballotfilemfrci  13249  ballotfilemth  13259  ballotfi  13260  ennnfonelemkh  13281  ennnfonelemhf1o  13282  setscomd  13371  ressressg  13406  qusex  13623  qusin  13624  grpinvalem  13682  grpinva  13683  grprida  13684  gzsumsplit1r  13692  isnsgrp  13698  sgrpass  13700  sgrp1  13703  sgrppropd  13705  mnd12g  13718  mndpropd  13730  imasmnd2  13736  mhmex  13746  mhmlin  13751  grprcan  13819  grpinvid1  13834  isgrpinv  13836  grplcan  13844  grpasscan1  13845  grplmulf1o  13856  grpinvadd  13860  grpinvsub  13864  grpsubsub4  13875  grppnpcan2  13876  grpnpncan  13877  dfgrp3mlem  13880  dfgrp3m  13881  grplactcnv  13884  imasgrp2  13890  mhmlem  13894  mhmid  13895  mhmmnd  13896  mulgnnp1  13910  mulg2  13911  mulgnn0p1  13913  mulgsubcl  13916  mulgneg  13920  mulgaddcomlem  13925  mulgaddcom  13926  mulgz  13930  mulgnn0dir  13932  mulgdirlem  13933  mulgdir  13934  mulgneg2  13936  mulgnnass  13937  mulgnn0ass  13938  mulgass  13939  mulgassr  13940  mulgmodid  13941  mulgsubdir  13942  submmulg  13946  isnsg3  13987  nmzsubg  13990  ssnmz  13991  0nsg  13994  eqger  14004  eqgid  14006  eqgcpbl  14008  ghmlin  14028  ghmmulg  14036  ghmnsgima  14048  ghmnsgpreima  14049  conjghm  14056  conjnmz  14059  ablsub2inv  14092  abladdsub4  14095  abladdsub  14096  ablpncan2  14097  ablpnpcan  14101  ablnncan  14102  ablnnncan1  14105  gzsumconst  14120  gzsumsnfd  14124  gzsumsplit0  14125  gzsumshift  14126  gzsumgsum  14132  gsummptfidmadd  14138  gsumconstcmn  14143  prdssgrpd  14168  prdsidlem  14170  prdsmndd  14171  prdsinvlem  14173  mgpress  14205  rngass  14213  rngdi  14214  rngdir  14215  rnglz  14219  rngmneg1  14221  rngsubdir  14226  rngpropd  14229  imasrng  14230  srgass  14249  srgmulgass  14267  srgpcomp  14268  srgpcompp  14269  srgpcomppsc  14270  ringpropd  14316  ringlz  14321  ring1eq0  14326  ringnegl  14329  ringmneg1  14331  ringsubdir  14335  mulgass2  14336  ring1  14337  imasring  14342  opprrng  14355  opprring  14357  unitgrp  14396  dvrcan1  14420  rdivmuldivd  14424  subrginv  14518  resrhm  14529  unitrrg  14549  aprlring  14573  islmod  14600  lmodlema  14601  islmodd  14602  lmod0vs  14630  lmodvs0  14631  lmodvsmmulgdi  14632  lmodvneg1  14639  lmodvsneg  14640  lmodsubvs  14652  lmodsubdi  14653  lmodsubdir  14654  lmodprop2d  14657  rmodislmodlem  14659  rmodislmod  14660  lsssetm  14665  islssmd  14668  lssclg  14673  lssvacl  14674  lss1d  14692  lsspropdg  14740  sraval  14746  rnglidlmcl  14789  znunit  14966  mplsubgfilemcl  15013  resttop  15194  restco  15198  restin  15200  lmfval  15217  cnprcl2k  15230  txrest  15300  txdis1cn  15302  cnmpt2res  15321  psmettri2  15352  psmettri  15354  xmettri2  15385  xmettri  15396  mettri  15397  metrtri  15401  blvalps  15412  blval  15413  xblss2  15429  blhalf  15432  comet  15523  xmetxp  15531  txmetcnp  15542  cnmet  15554  ioo2bl  15575  ivthreinc  15669  limcmpted  15687  limcimolemlt  15688  cnplimclemr  15693  limccnp2cntop  15701  reldvg  15703  dvfvalap  15705  dvidlemap  15715  dvidrelem  15716  dvidsslem  15717  dvconst  15718  dvconstre  15720  dvconstss  15722  dvcnp2cntop  15723  dvaddxxbr  15725  dvmulxxbr  15726  dvcoapbr  15731  dvcjbr  15732  dvexp  15735  dvrecap  15737  dvmptcmulcn  15745  dveflem  15750  plyval  15756  elply2  15759  elplyr  15764  elplyd  15765  ply1termlem  15766  plyaddlem1  15771  plymullem1  15772  plycoeid3  15781  plycjlemc  15784  dvply1  15789  sin0pilem1  15805  sinperlem  15832  ptolemy  15848  tangtx  15862  abssinper  15870  reexplog  15895  relogexp  15896  cxprec  15935  rpdivcxp  15936  cxpmul  15937  rpabscxpbnd  15965  rplogbval  15970  rplogbreexp  15978  rprelogbmul  15980  logbrec  15985  logbgcd1irraplemap  15994  binom4  16004  pellexlem2  16006  pellexlem3  16007  wilthlem1  16008  mpodvdsmulf1o  16018  sgmppw  16020  0sgmppw  16021  1sgmprm  16022  1sgm2ppw  16023  perfectlem1  16027  perfectlem2  16028  perfect  16029  lgslem1  16033  lgslem4  16036  lgsval  16037  lgsfvalg  16038  lgsval2lem  16043  lgsval4lem  16044  lgsvalmod  16052  lgsneg  16057  lgsneg1  16058  lgsmod  16059  lgsdilem  16060  lgsdir2lem4  16064  lgsdir2  16066  lgsdirprm  16067  lgsdir  16068  lgsne0  16071  lgssq  16073  lgssq2  16074  lgsmulsqcoprm  16079  lgsdirnn0  16080  lgsdinn0  16081  gausslemma2dlem1a  16091  gausslemma2dlem4  16097  gausslemma2dlem5a  16098  gausslemma2dlem5  16099  gausslemma2dlem6  16100  gausslemma2dlem7  16101  gausslemma2d  16102  lgseisenlem1  16103  lgseisenlem2  16104  lgseisenlem3  16105  lgseisenlem4  16106  lgseisen  16107  lgsquadlem1  16110  lgsquadlem2  16111  lgsquad2lem1  16114  lgsquad2lem2  16115  lgsquad3  16117  m1lgs  16118  2lgslem1a  16121  2lgslem1c  16123  2lgslem3a  16126  2lgslem3b  16127  2lgslem3c  16128  2lgslem3d  16129  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgslem3d1  16133  2lgsoddprmlem1  16138  2lgsoddprmlem2  16139  2lgsoddprmlem3  16144  2sqlem1  16147  2sqlem2  16148  mul2sq  16149  2sqlem3  16150  2sqlem4  16151  2sqlem8  16156  2sqlem9  16157  2sqlem10  16158  vdegp1bid  16470  uspgr2wlkeqi  16522  isclwwlk  16549  clwwlkccatlem  16555  clwwlknonex2  16594  repiecele0  16980  repiecege0  16981  repiecef  16982  trilpolemeq1  16994  trilpolemlt1  16995  trirec0xor  16999  apdifflemf  17000  apdiff  17002  qdiff  17003