Theorem oveq1d 5940

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

Syntax hints:   → wi 4   = wceq 1364  (class class class)co 5925

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928

This theorem is referenced by:  fvoveq1d  5947  csbov2g  5967  caovassg  6086  caovdig  6102  caovdirg  6105  caov12d  6109  caov31d  6110  caov411d  6113  caofinvl  6165  omsuc  6539  nnmsucr  6555  nnm1  6592  nnm2  6593  ecovass  6712  ecoviass  6713  ecovdi  6714  ecovidi  6715  isacnm  7288  addasspig  7416  mulasspig  7418  mulpipq2  7457  distrnqg  7473  ltsonq  7484  ltanqg  7486  ltmnqg  7487  ltexnqq  7494  archnqq  7503  prarloclemarch2  7505  enq0sym  7518  addnq0mo  7533  mulnq0mo  7534  addnnnq0  7535  nqpnq0nq  7539  nq0m0r  7542  nq0a0  7543  nnanq0  7544  distrnq0  7545  addassnq0  7548  addpinq1  7550  prarloclemlo  7580  prarloclem3  7583  prarloclem5  7586  prarloclemcalc  7588  addnqprllem  7613  addnqprulem  7614  appdivnq  7649  recexprlem1ssl  7719  recexprlem1ssu  7720  ltmprr  7728  cauappcvgprlemladdru  7742  cauappcvgprlem1  7745  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemcl  7762  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprlem1  7765  caucvgprprlemcbv  7773  caucvgprprlemval  7774  caucvgprprlemexb  7793  caucvgprprlem1  7795  addcmpblnr  7825  mulcmpblnrlemg  7826  addsrmo  7829  mulsrmo  7830  addsrpr  7831  mulsrpr  7832  ltsrprg  7833  1idsr  7854  pn0sr  7857  recexgt0sr  7859  mulgt0sr  7864  srpospr  7869  prsradd  7872  caucvgsrlemfv  7877  caucvgsrlemcau  7879  caucvgsrlemgt1  7881  caucvgsrlemoffval  7882  caucvgsrlemoffcau  7884  caucvgsrlemoffres  7886  caucvgsrlembnd  7887  caucvgsr  7888  map2psrprg  7891  pitonnlem1p1  7932  pitonnlem2  7933  pitonn  7934  recidpirqlemcalc  7943  ax1rid  7963  axrnegex  7965  axcnre  7967  recriota  7976  nntopi  7980  axcaucvglemval  7983  axcaucvglemcau  7984  axcaucvglemres  7985  mul12  8174  mul4  8177  muladd11  8178  readdcan  8185  muladd11r  8201  add12  8203  cnegex  8223  addcan  8225  negeu  8236  pncan2  8252  addsubass  8255  addsub  8256  2addsub  8259  addsubeq4  8260  subid  8264  subid1  8265  npncan  8266  nppcan  8267  nnpcan  8268  nnncan1  8281  npncan3  8283  pnpcan  8284  pnncan  8286  ppncan  8287  addsub4  8288  negsub  8293  subneg  8294  subeqxfrd  8408  mvlraddd  8409  mvlladdd  8410  mvrraddd  8411  subaddeqd  8414  ine0  8439  mulneg1  8440  ltadd2  8465  apreap  8633  cru  8648  recexap  8699  mulcanapd  8707  div23ap  8737  div13ap  8739  divmulassap  8741  divmulasscomap  8742  divcanap4  8745  muldivdirap  8753  divsubdirap  8754  divmuldivap  8758  divdivdivap  8759  divcanap5  8760  divmul13ap  8761  divmuleqap  8763  divdiv32ap  8766  divcanap7  8767  dmdcanap  8768  divdivap1  8769  divdivap2  8770  divadddivap  8773  divsubdivap  8774  conjmulap  8775  divneg2ap  8782  subrecap  8885  mvllmulapd  8888  lt2mul2div  8925  nndivtr  9051  2halves  9239  halfaddsub  9244  subhalfhalf  9245  avgle1  9251  avgle2  9252  div4p1lem1div2  9264  un0addcl  9301  un0mulcl  9302  peano2z  9381  zneo  9446  nneoor  9447  nneo  9448  zeo  9450  zeo2  9451  deceq1  9480  qreccl  9735  xaddcom  9955  xnegdi  9962  xaddass  9963  xaddass2  9964  xpncan  9965  xleadd1a  9967  xltadd1  9970  xposdif  9976  xadd4d  9979  lincmb01cmp  10097  iccf1o  10098  fz0to4untppr  10218  fzosubel3  10291  qavgle  10367  2tnp1ge0ge0  10410  fldiv4p1lem1div2  10414  fldiv4lem1div2  10416  ceilqm1lt  10423  flqdiv  10432  modqlt  10444  modqdiffl  10446  modqcyc2  10471  modqaddabs  10473  mulqaddmodid  10475  mulp1mod1  10476  modqmuladd  10477  modqmuladdnn0  10479  qnegmod  10480  addmodid  10483  addmodidr  10484  modqadd2mod  10485  modqm1p1mod0  10486  modqmul12d  10489  modqnegd  10490  modqadd12d  10491  modqsub12d  10492  q2submod  10496  modqmulmodr  10501  modqaddmulmod  10502  modqsubdir  10504  modfzo0difsn  10506  modsumfzodifsn  10507  addmodlteq  10509  frecuzrdgsuc  10525  frecfzennn  10537  iseqovex  10569  seq3-1p  10601  seq3caopr2  10604  seqcaopr2g  10605  seq3caopr  10606  seqcaoprg  10607  seqf1oglem2a  10629  seqf1oglem1  10630  seqf1oglem2  10631  seq3id  10636  seq3homo  10638  seq3z  10639  seqhomog  10641  seqfeq4g  10642  expp1  10657  exprecap  10691  expaddzaplem  10693  expmulzap  10696  expdivap  10701  sqval  10708  sqsubswap  10710  sqdividap  10715  subsq  10757  subsq2  10758  binom2  10762  binom2sub  10764  mulbinom2  10767  binom3  10768  zesq  10769  bernneq2  10772  modqexp  10777  sqoddm1div8  10804  mulsubdivbinom2ap  10822  nn0opthlem1d  10831  nn0opthd  10833  nn0opth2d  10834  facp1  10841  facdiv  10849  facndiv  10850  faclbnd  10852  faclbnd2  10853  faclbnd3  10854  bcval  10860  bccmpl  10865  bcm1k  10871  bcp1n  10872  bcp1nk  10873  bcval5  10874  bcp1m1  10876  bcpasc  10877  bcn2m1  10880  hashprg  10919  hashdifpr  10931  hashfzo  10933  hashfzp1  10935  hashfz0  10936  hashxp  10937  zfz1isolemsplit  10949  zfz1isolem1  10951  seq3coll  10953  reval  11033  crre  11041  remim  11044  remul2  11057  immul2  11064  imval2  11078  cjdivap  11093  caucvgre  11165  cvg1nlemcau  11168  cvg1nlemres  11169  resqrexlemp1rp  11190  resqrexlemfp1  11193  resqrexlemover  11194  resqrexlemcalc1  11198  resqrexlemcalc3  11200  resqrexlemnm  11202  resqrexlemoverl  11205  resqrexlemglsq  11206  resqrexlemga  11207  resqrexlemsqa  11208  resqrexlemex  11209  resqrex  11210  sqrtdiv  11226  absvalsq  11237  absreimsq  11251  absdivap  11254  cau3lem  11298  maxabslemlub  11391  maxabslemval  11392  max0addsup  11403  minabs  11420  bdtrilem  11423  bdtri  11424  xrmaxaddlem  11444  xrmaxadd  11445  xrbdtri  11460  clim  11465  clim2  11467  climshftlemg  11486  climshft2  11490  climcn1  11492  climcn2  11493  subcn2  11495  reccn2ap  11497  climmulc2  11515  climsubc2  11517  clim2ser  11521  iser3shft  11530  climcau  11531  serf0  11536  fzosump1  11601  fsum1p  11602  fsump1  11604  sumsplitdc  11616  fsump1i  11617  mptfzshft  11626  fisum0diag2  11631  fsumconst  11638  fsumdifsnconst  11639  modfsummodlemstep  11641  modfsummod  11642  telfsumo  11650  fsumparts  11654  fsumrelem  11655  hash2iun1dif1  11664  binomlem  11667  binom  11668  binom1p  11669  binom1dif  11671  bcxmas  11673  isumsplit  11675  isum1p  11676  arisum  11682  arisum2  11683  trireciplem  11684  geoserap  11691  geolim  11695  geolim2  11696  georeclim  11697  geo2sum  11698  geoisum1  11703  cvgratnnlemseq  11710  cvgratnnlemsumlt  11712  cvgratnnlemfm  11713  cvgratz  11716  mertenslemi1  11719  mertenslem2  11720  mertensabs  11721  fprod1p  11783  fprodp1  11784  fprodcl2lem  11789  fprodfac  11799  fprodeq0  11801  fprodconst  11804  fprodrec  11813  fprodsplit1f  11818  fprodmodd  11825  efcllemp  11842  ef0lem  11844  efval  11845  esum  11846  ege2le3  11855  efaddlem  11858  efsep  11875  effsumlt  11876  eft0val  11877  efgt1p2  11879  efgt1p  11880  sinval  11886  cosval  11887  resinval  11899  recosval  11900  efi4p  11901  resin4p  11902  recos4p  11903  sinneg  11910  cosneg  11911  efival  11916  sinadd  11920  cosadd  11921  tanaddap  11923  sinmul  11928  cosmul  11929  cos2t  11934  cos2tsin  11935  ef01bndlem  11940  absefib  11955  demoivre  11957  demoivreALT  11958  eirraplem  11961  p1modz1  11978  dvdsmodexp  11979  moddvds  11983  mulmoddvds  12047  3dvds2dec  12050  zeo3  12052  odd2np1lem  12056  odd2np1  12057  oexpneg  12061  2tp1odd  12068  ltoddhalfle  12077  opoe  12079  opeo  12081  omeo  12082  m1expo  12084  m1exp1  12085  nn0o1gt2  12089  nn0o  12091  divalglemnn  12102  divalglemqt  12103  divalglemeunn  12105  divalglemex  12106  divalglemeuneg  12107  flodddiv4  12120  flodddiv4t2lthalf  12123  bitsp1o  12137  bitsmod  12140  bitsinv1lem  12145  gcdaddm  12178  bezoutlemnewy  12190  bezoutlema  12193  bezoutlemb  12194  bezoutlemex  12195  bezoutlemaz  12197  mulgcd  12210  gcddiv  12213  gcdmultiplez  12215  rpmulgcd  12220  rplpwr  12221  uzwodc  12231  lcmgcdlem  12272  lcmgcd  12273  divgcdcoprmex  12297  cncongr2  12299  prmexpb  12346  rpexp  12348  rpexp1i  12349  sqrt2irrlem  12356  oddpwdclemxy  12364  oddpwdclemndvds  12366  sqpweven  12370  2sqpwodd  12371  sqne2sq  12372  qmuldeneqnum  12390  nn0gcdsq  12395  zgcdsq  12396  numdensq  12397  dfphi2  12415  phiprmpw  12417  phiprm  12418  eulerthlema  12425  eulerthlemh  12426  eulerthlemth  12427  fermltl  12429  prmdiv  12430  prmdiveq  12431  prmdivdiv  12432  hashgcdlem  12433  odzval  12437  odzcllem  12438  odzdvds  12441  vfermltl  12447  powm2modprm  12448  reumodprminv  12449  modprm0  12450  nnnn0modprm0  12451  modprmn0modprm0  12452  coprimeprodsq  12453  coprimeprodsq2  12454  pythagtriplem1  12461  pythagtriplem3  12463  pythagtriplem4  12464  pythagtriplem6  12466  pythagtriplem7  12467  pythagtriplem12  12471  pythagtriplem14  12473  pythagtriplem15  12474  pythagtriplem16  12475  pythagtriplem17  12476  pythagtriplem18  12477  pceu  12491  pczpre  12493  pcdiv  12498  pcqdiv  12503  pcrec  12504  pczndvds  12512  pcneg  12521  pc2dvds  12526  pcprmpw2  12529  pcaddlem  12535  pcadd  12536  fldivp1  12544  pockthlem  12552  pockthi  12554  4sqlem5  12578  4sqlem9  12582  4sqlem10  12583  4sqlem2  12585  4sqlem3  12586  4sqlem4  12588  mul4sqlem  12589  4sqlem11  12597  4sqlem12  12598  4sqlem14  12600  4sqlem15  12601  4sqlem17  12603  4sqlem19  12605  ennnfonelemkh  12656  ennnfonelemhf1o  12657  setscomd  12746  ressressg  12780  qusex  13029  qusin  13030  grpinvalem  13089  grpinva  13090  grprida  13091  gsumsplit1r  13102  isnsgrp  13110  sgrpass  13112  sgrp1  13115  sgrppropd  13117  prdssgrpd  13119  mnd12g  13132  mndpropd  13144  prdsidlem  13151  prdsmndd  13152  imasmnd2  13156  mhmex  13166  mhmlin  13171  grprcan  13241  grpinvid1  13256  isgrpinv  13258  grplcan  13266  grpasscan1  13267  grplmulf1o  13278  grpinvadd  13282  grpinvsub  13286  grpsubsub4  13297  grppnpcan2  13298  grpnpncan  13299  dfgrp3mlem  13302  dfgrp3m  13303  grplactcnv  13306  prdsinvlem  13312  imasgrp2  13318  mhmlem  13322  mhmid  13323  mhmmnd  13324  mulgnnp1  13338  mulg2  13339  mulgnn0p1  13341  mulgsubcl  13344  mulgneg  13348  mulgaddcomlem  13353  mulgaddcom  13354  mulgz  13358  mulgnn0dir  13360  mulgdirlem  13361  mulgdir  13362  mulgneg2  13364  mulgnnass  13365  mulgnn0ass  13366  mulgass  13367  mulgassr  13368  mulgmodid  13369  mulgsubdir  13370  submmulg  13374  isnsg3  13415  nmzsubg  13418  ssnmz  13419  0nsg  13422  eqger  13432  eqgid  13434  eqgcpbl  13436  ghmlin  13456  ghmmulg  13464  ghmnsgima  13476  ghmnsgpreima  13477  conjghm  13484  conjnmz  13487  ablsub2inv  13519  abladdsub4  13522  abladdsub  13523  ablpncan2  13524  ablpnpcan  13528  ablnncan  13529  ablnnncan1  13532  gsumfzconst  13549  gsumfzsnfd  13553  mgpress  13565  rngass  13573  rngdi  13574  rngdir  13575  rnglz  13579  rngmneg1  13581  rngsubdir  13586  rngpropd  13589  imasrng  13590  srgass  13605  srgmulgass  13623  srgpcomp  13624  srgpcompp  13625  srgpcomppsc  13626  ringpropd  13672  ringlz  13677  ring1eq0  13682  ringnegl  13685  ringmneg1  13687  ringsubdir  13691  mulgass2  13692  ring1  13693  imasring  13698  opprrng  13711  opprring  13713  unitgrp  13750  dvrcan1  13774  rdivmuldivd  13778  subrginv  13871  resrhm  13882  unitrrg  13901  islmod  13925  lmodlema  13926  islmodd  13927  lmod0vs  13955  lmodvs0  13956  lmodvsmmulgdi  13957  lmodvneg1  13964  lmodvsneg  13965  lmodsubvs  13977  lmodsubdi  13978  lmodsubdir  13979  lmodprop2d  13982  rmodislmodlem  13984  rmodislmod  13985  lsssetm  13990  islssmd  13993  lssclg  13998  lssvacl  13999  lss1d  14017  lsspropdg  14065  sraval  14071  rnglidlmcl  14114  gsumfzfsumlemm  14221  znunit  14293  mplsubgfilemcl  14333  resttop  14514  restco  14518  restin  14520  lmfval  14536  cnprcl2k  14550  txrest  14620  txdis1cn  14622  cnmpt2res  14641  psmettri2  14672  psmettri  14674  xmettri2  14705  xmettri  14716  mettri  14717  metrtri  14721  blvalps  14732  blval  14733  xblss2  14749  blhalf  14752  comet  14843  xmetxp  14851  txmetcnp  14862  cnmet  14874  ioo2bl  14895  ivthreinc  14989  limcmpted  15007  limcimolemlt  15008  cnplimclemr  15013  limccnp2cntop  15021  reldvg  15023  dvfvalap  15025  dvidlemap  15035  dvidrelem  15036  dvidsslem  15037  dvconst  15038  dvconstre  15040  dvconstss  15042  dvcnp2cntop  15043  dvaddxxbr  15045  dvmulxxbr  15046  dvcoapbr  15051  dvcjbr  15052  dvexp  15055  dvrecap  15057  dvmptcmulcn  15065  dveflem  15070  plyval  15076  elply2  15079  elplyr  15084  elplyd  15085  ply1termlem  15086  plyaddlem1  15091  plymullem1  15092  plycoeid3  15101  plycjlemc  15104  dvply1  15109  sin0pilem1  15125  sinperlem  15152  ptolemy  15168  tangtx  15182  abssinper  15190  reexplog  15215  relogexp  15216  cxprec  15254  rpdivcxp  15255  cxpmul  15256  rpabscxpbnd  15284  rplogbval  15289  rplogbreexp  15297  rprelogbmul  15299  logbrec  15304  logbgcd1irraplemap  15313  binom4  15323  wilthlem1  15324  mpodvdsmulf1o  15334  sgmppw  15336  0sgmppw  15337  1sgmprm  15338  1sgm2ppw  15339  perfectlem1  15343  perfectlem2  15344  perfect  15345  lgslem1  15349  lgslem4  15352  lgsval  15353  lgsfvalg  15354  lgsval2lem  15359  lgsval4lem  15360  lgsvalmod  15368  lgsneg  15373  lgsneg1  15374  lgsmod  15375  lgsdilem  15376  lgsdir2lem4  15380  lgsdir2  15382  lgsdirprm  15383  lgsdir  15384  lgsne0  15387  lgssq  15389  lgssq2  15390  lgsmulsqcoprm  15395  lgsdirnn0  15396  lgsdinn0  15397  gausslemma2dlem1a  15407  gausslemma2dlem4  15413  gausslemma2dlem5a  15414  gausslemma2dlem5  15415  gausslemma2dlem6  15416  gausslemma2dlem7  15417  gausslemma2d  15418  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisenlem4  15422  lgseisen  15423  lgsquadlem1  15426  lgsquadlem2  15427  lgsquad2lem1  15430  lgsquad2lem2  15431  lgsquad3  15433  m1lgs  15434  2lgslem1a  15437  2lgslem1c  15439  2lgslem3a  15442  2lgslem3b  15443  2lgslem3c  15444  2lgslem3d  15445  2lgslem3a1  15446  2lgslem3b1  15447  2lgslem3c1  15448  2lgslem3d1  15449  2lgsoddprmlem1  15454  2lgsoddprmlem2  15455  2lgsoddprmlem3  15460  2sqlem1  15463  2sqlem2  15464  mul2sq  15465  2sqlem3  15466  2sqlem4  15467  2sqlem8  15472  2sqlem9  15473  2sqlem10  15474  trilpolemeq1  15797  trilpolemlt1  15798  trirec0xor  15802  apdifflemf  15803  apdiff  15805