Theorem oveq1d 6015

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

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

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 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3888  df-br 4083  df-iota 5277  df-fv 5325  df-ov 6003

This theorem is referenced by:  fvoveq1d  6022  csbov2g  6042  caovassg  6163  caovdig  6179  caovdirg  6182  caov12d  6186  caov31d  6187  caov411d  6190  caofinvl  6242  omsuc  6616  nnmsucr  6632  nnm1  6669  nnm2  6670  ecovass  6789  ecoviass  6790  ecovdi  6791  ecovidi  6792  isacnm  7381  addasspig  7513  mulasspig  7515  mulpipq2  7554  distrnqg  7570  ltsonq  7581  ltanqg  7583  ltmnqg  7584  ltexnqq  7591  archnqq  7600  prarloclemarch2  7602  enq0sym  7615  addnq0mo  7630  mulnq0mo  7631  addnnnq0  7632  nqpnq0nq  7636  nq0m0r  7639  nq0a0  7640  nnanq0  7641  distrnq0  7642  addassnq0  7645  addpinq1  7647  prarloclemlo  7677  prarloclem3  7680  prarloclem5  7683  prarloclemcalc  7685  addnqprllem  7710  addnqprulem  7711  appdivnq  7746  recexprlem1ssl  7816  recexprlem1ssu  7817  ltmprr  7825  cauappcvgprlemladdru  7839  cauappcvgprlem1  7842  caucvgprlemnkj  7849  caucvgprlemnbj  7850  caucvgprlemcl  7859  caucvgprlemladdfu  7860  caucvgprlemladdrl  7861  caucvgprlem1  7862  caucvgprprlemcbv  7870  caucvgprprlemval  7871  caucvgprprlemexb  7890  caucvgprprlem1  7892  addcmpblnr  7922  mulcmpblnrlemg  7923  addsrmo  7926  mulsrmo  7927  addsrpr  7928  mulsrpr  7929  ltsrprg  7930  1idsr  7951  pn0sr  7954  recexgt0sr  7956  mulgt0sr  7961  srpospr  7966  prsradd  7969  caucvgsrlemfv  7974  caucvgsrlemcau  7976  caucvgsrlemgt1  7978  caucvgsrlemoffval  7979  caucvgsrlemoffcau  7981  caucvgsrlemoffres  7983  caucvgsrlembnd  7984  caucvgsr  7985  map2psrprg  7988  pitonnlem1p1  8029  pitonnlem2  8030  pitonn  8031  recidpirqlemcalc  8040  ax1rid  8060  axrnegex  8062  axcnre  8064  recriota  8073  nntopi  8077  axcaucvglemval  8080  axcaucvglemcau  8081  axcaucvglemres  8082  mul12  8271  mul4  8274  muladd11  8275  readdcan  8282  muladd11r  8298  add12  8300  cnegex  8320  addcan  8322  negeu  8333  pncan2  8349  addsubass  8352  addsub  8353  2addsub  8356  addsubeq4  8357  subid  8361  subid1  8362  npncan  8363  nppcan  8364  nnpcan  8365  nnncan1  8378  npncan3  8380  pnpcan  8381  pnncan  8383  ppncan  8384  addsub4  8385  negsub  8390  subneg  8391  subeqxfrd  8505  mvlraddd  8506  mvlladdd  8507  mvrraddd  8508  subaddeqd  8511  ine0  8536  mulneg1  8537  ltadd2  8562  apreap  8730  cru  8745  recexap  8796  mulcanapd  8804  div23ap  8834  div13ap  8836  divmulassap  8838  divmulasscomap  8839  divcanap4  8842  muldivdirap  8850  divsubdirap  8851  divmuldivap  8855  divdivdivap  8856  divcanap5  8857  divmul13ap  8858  divmuleqap  8860  divdiv32ap  8863  divcanap7  8864  dmdcanap  8865  divdivap1  8866  divdivap2  8867  divadddivap  8870  divsubdivap  8871  conjmulap  8872  divneg2ap  8879  subrecap  8982  mvllmulapd  8985  lt2mul2div  9022  nndivtr  9148  2halves  9336  halfaddsub  9341  subhalfhalf  9342  avgle1  9348  avgle2  9349  div4p1lem1div2  9361  un0addcl  9398  un0mulcl  9399  peano2z  9478  zneo  9544  nneoor  9545  nneo  9546  zeo  9548  zeo2  9549  deceq1  9578  qreccl  9833  xaddcom  10053  xnegdi  10060  xaddass  10061  xaddass2  10062  xpncan  10063  xleadd1a  10065  xltadd1  10068  xposdif  10074  xadd4d  10077  lincmb01cmp  10195  iccf1o  10196  fz0to4untppr  10316  fzo0addel  10389  fzosubel3  10397  qavgle  10473  2tnp1ge0ge0  10516  fldiv4p1lem1div2  10520  fldiv4lem1div2  10522  ceilqm1lt  10529  flqdiv  10538  modqlt  10550  modqdiffl  10552  modqcyc2  10577  modqaddabs  10579  mulqaddmodid  10581  mulp1mod1  10582  modqmuladd  10583  modqmuladdnn0  10585  qnegmod  10586  addmodid  10589  addmodidr  10590  modqadd2mod  10591  modqm1p1mod0  10592  modqmul12d  10595  modqnegd  10596  modqadd12d  10597  modqsub12d  10598  q2submod  10602  modqmulmodr  10607  modqaddmulmod  10608  modqsubdir  10610  modfzo0difsn  10612  modsumfzodifsn  10613  addmodlteq  10615  frecuzrdgsuc  10631  frecfzennn  10643  iseqovex  10675  seq3-1p  10707  seq3caopr2  10710  seqcaopr2g  10711  seq3caopr  10712  seqcaoprg  10713  seqf1oglem2a  10735  seqf1oglem1  10736  seqf1oglem2  10737  seq3id  10742  seq3homo  10744  seq3z  10745  seqhomog  10747  seqfeq4g  10748  expp1  10763  exprecap  10797  expaddzaplem  10799  expmulzap  10802  expdivap  10807  sqval  10814  sqsubswap  10816  sqdividap  10821  subsq  10863  subsq2  10864  binom2  10868  binom2sub  10870  mulbinom2  10873  binom3  10874  zesq  10875  bernneq2  10878  modqexp  10883  sqoddm1div8  10910  mulsubdivbinom2ap  10928  nn0opthlem1d  10937  nn0opthd  10939  nn0opth2d  10940  facp1  10947  facdiv  10955  facndiv  10956  faclbnd  10958  faclbnd2  10959  faclbnd3  10960  bcval  10966  bccmpl  10971  bcm1k  10977  bcp1n  10978  bcp1nk  10979  bcval5  10980  bcp1m1  10982  bcpasc  10983  bcn2m1  10986  hashprg  11025  hashdifpr  11037  hashfzo  11039  hashfzp1  11041  hashfz0  11042  hashxp  11043  zfz1isolemsplit  11055  zfz1isolem1  11057  seq3coll  11059  lswwrd  11113  ccatfvalfi  11122  ccatass  11138  lswccatn0lsw  11141  ccatswrd  11197  ccatpfx  11228  swrdpfx  11234  pfxpfx  11235  ccats1pfxeq  11241  wrdeqs1cat  11247  wrdind  11249  wrd2ind  11250  pfxccatpfx2  11264  pfxccatin12d  11272  cats1catd  11295  cats2catd  11296  s2leng  11316  reval  11355  crre  11363  remim  11366  remul2  11379  immul2  11386  imval2  11400  cjdivap  11415  caucvgre  11487  cvg1nlemcau  11490  cvg1nlemres  11491  resqrexlemp1rp  11512  resqrexlemfp1  11515  resqrexlemover  11516  resqrexlemcalc1  11520  resqrexlemcalc3  11522  resqrexlemnm  11524  resqrexlemoverl  11527  resqrexlemglsq  11528  resqrexlemga  11529  resqrexlemsqa  11530  resqrexlemex  11531  resqrex  11532  sqrtdiv  11548  absvalsq  11559  absreimsq  11573  absdivap  11576  cau3lem  11620  maxabslemlub  11713  maxabslemval  11714  max0addsup  11725  minabs  11742  bdtrilem  11745  bdtri  11746  xrmaxaddlem  11766  xrmaxadd  11767  xrbdtri  11782  clim  11787  clim2  11789  climshftlemg  11808  climshft2  11812  climcn1  11814  climcn2  11815  subcn2  11817  reccn2ap  11819  climmulc2  11837  climsubc2  11839  clim2ser  11843  iser3shft  11852  climcau  11853  serf0  11858  fzosump1  11923  fsum1p  11924  fsump1  11926  sumsplitdc  11938  fsump1i  11939  mptfzshft  11948  fisum0diag2  11953  fsumconst  11960  fsumdifsnconst  11961  modfsummodlemstep  11963  modfsummod  11964  telfsumo  11972  fsumparts  11976  fsumrelem  11977  hash2iun1dif1  11986  binomlem  11989  binom  11990  binom1p  11991  binom1dif  11993  bcxmas  11995  isumsplit  11997  isum1p  11998  arisum  12004  arisum2  12005  trireciplem  12006  geoserap  12013  geolim  12017  geolim2  12018  georeclim  12019  geo2sum  12020  geoisum1  12025  cvgratnnlemseq  12032  cvgratnnlemsumlt  12034  cvgratnnlemfm  12035  cvgratz  12038  mertenslemi1  12041  mertenslem2  12042  mertensabs  12043  fprod1p  12105  fprodp1  12106  fprodcl2lem  12111  fprodfac  12121  fprodeq0  12123  fprodconst  12126  fprodrec  12135  fprodsplit1f  12140  fprodmodd  12147  efcllemp  12164  ef0lem  12166  efval  12167  esum  12168  ege2le3  12177  efaddlem  12180  efsep  12197  effsumlt  12198  eft0val  12199  efgt1p2  12201  efgt1p  12202  sinval  12208  cosval  12209  resinval  12221  recosval  12222  efi4p  12223  resin4p  12224  recos4p  12225  sinneg  12232  cosneg  12233  efival  12238  sinadd  12242  cosadd  12243  tanaddap  12245  sinmul  12250  cosmul  12251  cos2t  12256  cos2tsin  12257  ef01bndlem  12262  absefib  12277  demoivre  12279  demoivreALT  12280  eirraplem  12283  p1modz1  12300  dvdsmodexp  12301  moddvds  12305  mulmoddvds  12369  3dvds2dec  12372  zeo3  12374  odd2np1lem  12378  odd2np1  12379  oexpneg  12383  2tp1odd  12390  ltoddhalfle  12399  opoe  12401  opeo  12403  omeo  12404  m1expo  12406  m1exp1  12407  nn0o1gt2  12411  nn0o  12413  divalglemnn  12424  divalglemqt  12425  divalglemeunn  12427  divalglemex  12428  divalglemeuneg  12429  flodddiv4  12442  flodddiv4t2lthalf  12445  bitsp1o  12459  bitsmod  12462  bitsinv1lem  12467  gcdaddm  12500  bezoutlemnewy  12512  bezoutlema  12515  bezoutlemb  12516  bezoutlemex  12517  bezoutlemaz  12519  mulgcd  12532  gcddiv  12535  gcdmultiplez  12537  rpmulgcd  12542  rplpwr  12543  uzwodc  12553  lcmgcdlem  12594  lcmgcd  12595  divgcdcoprmex  12619  cncongr2  12621  prmexpb  12668  rpexp  12670  rpexp1i  12671  sqrt2irrlem  12678  oddpwdclemxy  12686  oddpwdclemndvds  12688  sqpweven  12692  2sqpwodd  12693  sqne2sq  12694  qmuldeneqnum  12712  nn0gcdsq  12717  zgcdsq  12718  numdensq  12719  dfphi2  12737  phiprmpw  12739  phiprm  12740  eulerthlema  12747  eulerthlemh  12748  eulerthlemth  12749  fermltl  12751  prmdiv  12752  prmdiveq  12753  prmdivdiv  12754  hashgcdlem  12755  odzval  12759  odzcllem  12760  odzdvds  12763  vfermltl  12769  powm2modprm  12770  reumodprminv  12771  modprm0  12772  nnnn0modprm0  12773  modprmn0modprm0  12774  coprimeprodsq  12775  coprimeprodsq2  12776  pythagtriplem1  12783  pythagtriplem3  12785  pythagtriplem4  12786  pythagtriplem6  12788  pythagtriplem7  12789  pythagtriplem12  12793  pythagtriplem14  12795  pythagtriplem15  12796  pythagtriplem16  12797  pythagtriplem17  12798  pythagtriplem18  12799  pceu  12813  pczpre  12815  pcdiv  12820  pcqdiv  12825  pcrec  12826  pczndvds  12834  pcneg  12843  pc2dvds  12848  pcprmpw2  12851  pcaddlem  12857  pcadd  12858  fldivp1  12866  pockthlem  12874  pockthi  12876  4sqlem5  12900  4sqlem9  12904  4sqlem10  12905  4sqlem2  12907  4sqlem3  12908  4sqlem4  12910  mul4sqlem  12911  4sqlem11  12919  4sqlem12  12920  4sqlem14  12922  4sqlem15  12923  4sqlem17  12925  4sqlem19  12927  ennnfonelemkh  12978  ennnfonelemhf1o  12979  setscomd  13068  ressressg  13103  qusex  13353  qusin  13354  grpinvalem  13413  grpinva  13414  grprida  13415  gsumsplit1r  13426  isnsgrp  13434  sgrpass  13436  sgrp1  13439  sgrppropd  13441  prdssgrpd  13443  mnd12g  13456  mndpropd  13468  prdsidlem  13475  prdsmndd  13476  imasmnd2  13480  mhmex  13490  mhmlin  13495  grprcan  13565  grpinvid1  13580  isgrpinv  13582  grplcan  13590  grpasscan1  13591  grplmulf1o  13602  grpinvadd  13606  grpinvsub  13610  grpsubsub4  13621  grppnpcan2  13622  grpnpncan  13623  dfgrp3mlem  13626  dfgrp3m  13627  grplactcnv  13630  prdsinvlem  13636  imasgrp2  13642  mhmlem  13646  mhmid  13647  mhmmnd  13648  mulgnnp1  13662  mulg2  13663  mulgnn0p1  13665  mulgsubcl  13668  mulgneg  13672  mulgaddcomlem  13677  mulgaddcom  13678  mulgz  13682  mulgnn0dir  13684  mulgdirlem  13685  mulgdir  13686  mulgneg2  13688  mulgnnass  13689  mulgnn0ass  13690  mulgass  13691  mulgassr  13692  mulgmodid  13693  mulgsubdir  13694  submmulg  13698  isnsg3  13739  nmzsubg  13742  ssnmz  13743  0nsg  13746  eqger  13756  eqgid  13758  eqgcpbl  13760  ghmlin  13780  ghmmulg  13788  ghmnsgima  13800  ghmnsgpreima  13801  conjghm  13808  conjnmz  13811  ablsub2inv  13843  abladdsub4  13846  abladdsub  13847  ablpncan2  13848  ablpnpcan  13852  ablnncan  13853  ablnnncan1  13856  gsumfzconst  13873  gsumfzsnfd  13877  mgpress  13889  rngass  13897  rngdi  13898  rngdir  13899  rnglz  13903  rngmneg1  13905  rngsubdir  13910  rngpropd  13913  imasrng  13914  srgass  13929  srgmulgass  13947  srgpcomp  13948  srgpcompp  13949  srgpcomppsc  13950  ringpropd  13996  ringlz  14001  ring1eq0  14006  ringnegl  14009  ringmneg1  14011  ringsubdir  14015  mulgass2  14016  ring1  14017  imasring  14022  opprrng  14035  opprring  14037  unitgrp  14074  dvrcan1  14098  rdivmuldivd  14102  subrginv  14195  resrhm  14206  unitrrg  14225  islmod  14249  lmodlema  14250  islmodd  14251  lmod0vs  14279  lmodvs0  14280  lmodvsmmulgdi  14281  lmodvneg1  14288  lmodvsneg  14289  lmodsubvs  14301  lmodsubdi  14302  lmodsubdir  14303  lmodprop2d  14306  rmodislmodlem  14308  rmodislmod  14309  lsssetm  14314  islssmd  14317  lssclg  14322  lssvacl  14323  lss1d  14341  lsspropdg  14389  sraval  14395  rnglidlmcl  14438  gsumfzfsumlemm  14545  znunit  14617  mplsubgfilemcl  14657  resttop  14838  restco  14842  restin  14844  lmfval  14860  cnprcl2k  14874  txrest  14944  txdis1cn  14946  cnmpt2res  14965  psmettri2  14996  psmettri  14998  xmettri2  15029  xmettri  15040  mettri  15041  metrtri  15045  blvalps  15056  blval  15057  xblss2  15073  blhalf  15076  comet  15167  xmetxp  15175  txmetcnp  15186  cnmet  15198  ioo2bl  15219  ivthreinc  15313  limcmpted  15331  limcimolemlt  15332  cnplimclemr  15337  limccnp2cntop  15345  reldvg  15347  dvfvalap  15349  dvidlemap  15359  dvidrelem  15360  dvidsslem  15361  dvconst  15362  dvconstre  15364  dvconstss  15366  dvcnp2cntop  15367  dvaddxxbr  15369  dvmulxxbr  15370  dvcoapbr  15375  dvcjbr  15376  dvexp  15379  dvrecap  15381  dvmptcmulcn  15389  dveflem  15394  plyval  15400  elply2  15403  elplyr  15408  elplyd  15409  ply1termlem  15410  plyaddlem1  15415  plymullem1  15416  plycoeid3  15425  plycjlemc  15428  dvply1  15433  sin0pilem1  15449  sinperlem  15476  ptolemy  15492  tangtx  15506  abssinper  15514  reexplog  15539  relogexp  15540  cxprec  15578  rpdivcxp  15579  cxpmul  15580  rpabscxpbnd  15608  rplogbval  15613  rplogbreexp  15621  rprelogbmul  15623  logbrec  15628  logbgcd1irraplemap  15637  binom4  15647  wilthlem1  15648  mpodvdsmulf1o  15658  sgmppw  15660  0sgmppw  15661  1sgmprm  15662  1sgm2ppw  15663  perfectlem1  15667  perfectlem2  15668  perfect  15669  lgslem1  15673  lgslem4  15676  lgsval  15677  lgsfvalg  15678  lgsval2lem  15683  lgsval4lem  15684  lgsvalmod  15692  lgsneg  15697  lgsneg1  15698  lgsmod  15699  lgsdilem  15700  lgsdir2lem4  15704  lgsdir2  15706  lgsdirprm  15707  lgsdir  15708  lgsne0  15711  lgssq  15713  lgssq2  15714  lgsmulsqcoprm  15719  lgsdirnn0  15720  lgsdinn0  15721  gausslemma2dlem1a  15731  gausslemma2dlem4  15737  gausslemma2dlem5a  15738  gausslemma2dlem5  15739  gausslemma2dlem6  15740  gausslemma2dlem7  15741  gausslemma2d  15742  lgseisenlem1  15743  lgseisenlem2  15744  lgseisenlem3  15745  lgseisenlem4  15746  lgseisen  15747  lgsquadlem1  15750  lgsquadlem2  15751  lgsquad2lem1  15754  lgsquad2lem2  15755  lgsquad3  15757  m1lgs  15758  2lgslem1a  15761  2lgslem1c  15763  2lgslem3a  15766  2lgslem3b  15767  2lgslem3c  15768  2lgslem3d  15769  2lgslem3a1  15770  2lgslem3b1  15771  2lgslem3c1  15772  2lgslem3d1  15773  2lgsoddprmlem1  15778  2lgsoddprmlem2  15779  2lgsoddprmlem3  15784  2sqlem1  15787  2sqlem2  15788  mul2sq  15789  2sqlem3  15790  2sqlem4  15791  2sqlem8  15796  2sqlem9  15797  2sqlem10  15798  trilpolemeq1  16367  trilpolemlt1  16368  trirec0xor  16372  apdifflemf  16373  apdiff  16375