Theorem oveq1d 5959

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

Syntax hints:   → wi 4   = wceq 1373  (class class class)co 5944

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-rex 2490  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-uni 3851  df-br 4045  df-iota 5232  df-fv 5279  df-ov 5947

This theorem is referenced by:  fvoveq1d  5966  csbov2g  5986  caovassg  6105  caovdig  6121  caovdirg  6124  caov12d  6128  caov31d  6129  caov411d  6132  caofinvl  6184  omsuc  6558  nnmsucr  6574  nnm1  6611  nnm2  6612  ecovass  6731  ecoviass  6732  ecovdi  6733  ecovidi  6734  isacnm  7315  addasspig  7443  mulasspig  7445  mulpipq2  7484  distrnqg  7500  ltsonq  7511  ltanqg  7513  ltmnqg  7514  ltexnqq  7521  archnqq  7530  prarloclemarch2  7532  enq0sym  7545  addnq0mo  7560  mulnq0mo  7561  addnnnq0  7562  nqpnq0nq  7566  nq0m0r  7569  nq0a0  7570  nnanq0  7571  distrnq0  7572  addassnq0  7575  addpinq1  7577  prarloclemlo  7607  prarloclem3  7610  prarloclem5  7613  prarloclemcalc  7615  addnqprllem  7640  addnqprulem  7641  appdivnq  7676  recexprlem1ssl  7746  recexprlem1ssu  7747  ltmprr  7755  cauappcvgprlemladdru  7769  cauappcvgprlem1  7772  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemcl  7789  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprlem1  7792  caucvgprprlemcbv  7800  caucvgprprlemval  7801  caucvgprprlemexb  7820  caucvgprprlem1  7822  addcmpblnr  7852  mulcmpblnrlemg  7853  addsrmo  7856  mulsrmo  7857  addsrpr  7858  mulsrpr  7859  ltsrprg  7860  1idsr  7881  pn0sr  7884  recexgt0sr  7886  mulgt0sr  7891  srpospr  7896  prsradd  7899  caucvgsrlemfv  7904  caucvgsrlemcau  7906  caucvgsrlemgt1  7908  caucvgsrlemoffval  7909  caucvgsrlemoffcau  7911  caucvgsrlemoffres  7913  caucvgsrlembnd  7914  caucvgsr  7915  map2psrprg  7918  pitonnlem1p1  7959  pitonnlem2  7960  pitonn  7961  recidpirqlemcalc  7970  ax1rid  7990  axrnegex  7992  axcnre  7994  recriota  8003  nntopi  8007  axcaucvglemval  8010  axcaucvglemcau  8011  axcaucvglemres  8012  mul12  8201  mul4  8204  muladd11  8205  readdcan  8212  muladd11r  8228  add12  8230  cnegex  8250  addcan  8252  negeu  8263  pncan2  8279  addsubass  8282  addsub  8283  2addsub  8286  addsubeq4  8287  subid  8291  subid1  8292  npncan  8293  nppcan  8294  nnpcan  8295  nnncan1  8308  npncan3  8310  pnpcan  8311  pnncan  8313  ppncan  8314  addsub4  8315  negsub  8320  subneg  8321  subeqxfrd  8435  mvlraddd  8436  mvlladdd  8437  mvrraddd  8438  subaddeqd  8441  ine0  8466  mulneg1  8467  ltadd2  8492  apreap  8660  cru  8675  recexap  8726  mulcanapd  8734  div23ap  8764  div13ap  8766  divmulassap  8768  divmulasscomap  8769  divcanap4  8772  muldivdirap  8780  divsubdirap  8781  divmuldivap  8785  divdivdivap  8786  divcanap5  8787  divmul13ap  8788  divmuleqap  8790  divdiv32ap  8793  divcanap7  8794  dmdcanap  8795  divdivap1  8796  divdivap2  8797  divadddivap  8800  divsubdivap  8801  conjmulap  8802  divneg2ap  8809  subrecap  8912  mvllmulapd  8915  lt2mul2div  8952  nndivtr  9078  2halves  9266  halfaddsub  9271  subhalfhalf  9272  avgle1  9278  avgle2  9279  div4p1lem1div2  9291  un0addcl  9328  un0mulcl  9329  peano2z  9408  zneo  9474  nneoor  9475  nneo  9476  zeo  9478  zeo2  9479  deceq1  9508  qreccl  9763  xaddcom  9983  xnegdi  9990  xaddass  9991  xaddass2  9992  xpncan  9993  xleadd1a  9995  xltadd1  9998  xposdif  10004  xadd4d  10007  lincmb01cmp  10125  iccf1o  10126  fz0to4untppr  10246  fzo0addel  10317  fzosubel3  10325  qavgle  10401  2tnp1ge0ge0  10444  fldiv4p1lem1div2  10448  fldiv4lem1div2  10450  ceilqm1lt  10457  flqdiv  10466  modqlt  10478  modqdiffl  10480  modqcyc2  10505  modqaddabs  10507  mulqaddmodid  10509  mulp1mod1  10510  modqmuladd  10511  modqmuladdnn0  10513  qnegmod  10514  addmodid  10517  addmodidr  10518  modqadd2mod  10519  modqm1p1mod0  10520  modqmul12d  10523  modqnegd  10524  modqadd12d  10525  modqsub12d  10526  q2submod  10530  modqmulmodr  10535  modqaddmulmod  10536  modqsubdir  10538  modfzo0difsn  10540  modsumfzodifsn  10541  addmodlteq  10543  frecuzrdgsuc  10559  frecfzennn  10571  iseqovex  10603  seq3-1p  10635  seq3caopr2  10638  seqcaopr2g  10639  seq3caopr  10640  seqcaoprg  10641  seqf1oglem2a  10663  seqf1oglem1  10664  seqf1oglem2  10665  seq3id  10670  seq3homo  10672  seq3z  10673  seqhomog  10675  seqfeq4g  10676  expp1  10691  exprecap  10725  expaddzaplem  10727  expmulzap  10730  expdivap  10735  sqval  10742  sqsubswap  10744  sqdividap  10749  subsq  10791  subsq2  10792  binom2  10796  binom2sub  10798  mulbinom2  10801  binom3  10802  zesq  10803  bernneq2  10806  modqexp  10811  sqoddm1div8  10838  mulsubdivbinom2ap  10856  nn0opthlem1d  10865  nn0opthd  10867  nn0opth2d  10868  facp1  10875  facdiv  10883  facndiv  10884  faclbnd  10886  faclbnd2  10887  faclbnd3  10888  bcval  10894  bccmpl  10899  bcm1k  10905  bcp1n  10906  bcp1nk  10907  bcval5  10908  bcp1m1  10910  bcpasc  10911  bcn2m1  10914  hashprg  10953  hashdifpr  10965  hashfzo  10967  hashfzp1  10969  hashfz0  10970  hashxp  10971  zfz1isolemsplit  10983  zfz1isolem1  10985  seq3coll  10987  lswwrd  11040  ccatfvalfi  11048  ccatass  11064  lswccatn0lsw  11067  ccatswrd  11123  reval  11160  crre  11168  remim  11171  remul2  11184  immul2  11191  imval2  11205  cjdivap  11220  caucvgre  11292  cvg1nlemcau  11295  cvg1nlemres  11296  resqrexlemp1rp  11317  resqrexlemfp1  11320  resqrexlemover  11321  resqrexlemcalc1  11325  resqrexlemcalc3  11327  resqrexlemnm  11329  resqrexlemoverl  11332  resqrexlemglsq  11333  resqrexlemga  11334  resqrexlemsqa  11335  resqrexlemex  11336  resqrex  11337  sqrtdiv  11353  absvalsq  11364  absreimsq  11378  absdivap  11381  cau3lem  11425  maxabslemlub  11518  maxabslemval  11519  max0addsup  11530  minabs  11547  bdtrilem  11550  bdtri  11551  xrmaxaddlem  11571  xrmaxadd  11572  xrbdtri  11587  clim  11592  clim2  11594  climshftlemg  11613  climshft2  11617  climcn1  11619  climcn2  11620  subcn2  11622  reccn2ap  11624  climmulc2  11642  climsubc2  11644  clim2ser  11648  iser3shft  11657  climcau  11658  serf0  11663  fzosump1  11728  fsum1p  11729  fsump1  11731  sumsplitdc  11743  fsump1i  11744  mptfzshft  11753  fisum0diag2  11758  fsumconst  11765  fsumdifsnconst  11766  modfsummodlemstep  11768  modfsummod  11769  telfsumo  11777  fsumparts  11781  fsumrelem  11782  hash2iun1dif1  11791  binomlem  11794  binom  11795  binom1p  11796  binom1dif  11798  bcxmas  11800  isumsplit  11802  isum1p  11803  arisum  11809  arisum2  11810  trireciplem  11811  geoserap  11818  geolim  11822  geolim2  11823  georeclim  11824  geo2sum  11825  geoisum1  11830  cvgratnnlemseq  11837  cvgratnnlemsumlt  11839  cvgratnnlemfm  11840  cvgratz  11843  mertenslemi1  11846  mertenslem2  11847  mertensabs  11848  fprod1p  11910  fprodp1  11911  fprodcl2lem  11916  fprodfac  11926  fprodeq0  11928  fprodconst  11931  fprodrec  11940  fprodsplit1f  11945  fprodmodd  11952  efcllemp  11969  ef0lem  11971  efval  11972  esum  11973  ege2le3  11982  efaddlem  11985  efsep  12002  effsumlt  12003  eft0val  12004  efgt1p2  12006  efgt1p  12007  sinval  12013  cosval  12014  resinval  12026  recosval  12027  efi4p  12028  resin4p  12029  recos4p  12030  sinneg  12037  cosneg  12038  efival  12043  sinadd  12047  cosadd  12048  tanaddap  12050  sinmul  12055  cosmul  12056  cos2t  12061  cos2tsin  12062  ef01bndlem  12067  absefib  12082  demoivre  12084  demoivreALT  12085  eirraplem  12088  p1modz1  12105  dvdsmodexp  12106  moddvds  12110  mulmoddvds  12174  3dvds2dec  12177  zeo3  12179  odd2np1lem  12183  odd2np1  12184  oexpneg  12188  2tp1odd  12195  ltoddhalfle  12204  opoe  12206  opeo  12208  omeo  12209  m1expo  12211  m1exp1  12212  nn0o1gt2  12216  nn0o  12218  divalglemnn  12229  divalglemqt  12230  divalglemeunn  12232  divalglemex  12233  divalglemeuneg  12234  flodddiv4  12247  flodddiv4t2lthalf  12250  bitsp1o  12264  bitsmod  12267  bitsinv1lem  12272  gcdaddm  12305  bezoutlemnewy  12317  bezoutlema  12320  bezoutlemb  12321  bezoutlemex  12322  bezoutlemaz  12324  mulgcd  12337  gcddiv  12340  gcdmultiplez  12342  rpmulgcd  12347  rplpwr  12348  uzwodc  12358  lcmgcdlem  12399  lcmgcd  12400  divgcdcoprmex  12424  cncongr2  12426  prmexpb  12473  rpexp  12475  rpexp1i  12476  sqrt2irrlem  12483  oddpwdclemxy  12491  oddpwdclemndvds  12493  sqpweven  12497  2sqpwodd  12498  sqne2sq  12499  qmuldeneqnum  12517  nn0gcdsq  12522  zgcdsq  12523  numdensq  12524  dfphi2  12542  phiprmpw  12544  phiprm  12545  eulerthlema  12552  eulerthlemh  12553  eulerthlemth  12554  fermltl  12556  prmdiv  12557  prmdiveq  12558  prmdivdiv  12559  hashgcdlem  12560  odzval  12564  odzcllem  12565  odzdvds  12568  vfermltl  12574  powm2modprm  12575  reumodprminv  12576  modprm0  12577  nnnn0modprm0  12578  modprmn0modprm0  12579  coprimeprodsq  12580  coprimeprodsq2  12581  pythagtriplem1  12588  pythagtriplem3  12590  pythagtriplem4  12591  pythagtriplem6  12593  pythagtriplem7  12594  pythagtriplem12  12598  pythagtriplem14  12600  pythagtriplem15  12601  pythagtriplem16  12602  pythagtriplem17  12603  pythagtriplem18  12604  pceu  12618  pczpre  12620  pcdiv  12625  pcqdiv  12630  pcrec  12631  pczndvds  12639  pcneg  12648  pc2dvds  12653  pcprmpw2  12656  pcaddlem  12662  pcadd  12663  fldivp1  12671  pockthlem  12679  pockthi  12681  4sqlem5  12705  4sqlem9  12709  4sqlem10  12710  4sqlem2  12712  4sqlem3  12713  4sqlem4  12715  mul4sqlem  12716  4sqlem11  12724  4sqlem12  12725  4sqlem14  12727  4sqlem15  12728  4sqlem17  12730  4sqlem19  12732  ennnfonelemkh  12783  ennnfonelemhf1o  12784  setscomd  12873  ressressg  12907  qusex  13157  qusin  13158  grpinvalem  13217  grpinva  13218  grprida  13219  gsumsplit1r  13230  isnsgrp  13238  sgrpass  13240  sgrp1  13243  sgrppropd  13245  prdssgrpd  13247  mnd12g  13260  mndpropd  13272  prdsidlem  13279  prdsmndd  13280  imasmnd2  13284  mhmex  13294  mhmlin  13299  grprcan  13369  grpinvid1  13384  isgrpinv  13386  grplcan  13394  grpasscan1  13395  grplmulf1o  13406  grpinvadd  13410  grpinvsub  13414  grpsubsub4  13425  grppnpcan2  13426  grpnpncan  13427  dfgrp3mlem  13430  dfgrp3m  13431  grplactcnv  13434  prdsinvlem  13440  imasgrp2  13446  mhmlem  13450  mhmid  13451  mhmmnd  13452  mulgnnp1  13466  mulg2  13467  mulgnn0p1  13469  mulgsubcl  13472  mulgneg  13476  mulgaddcomlem  13481  mulgaddcom  13482  mulgz  13486  mulgnn0dir  13488  mulgdirlem  13489  mulgdir  13490  mulgneg2  13492  mulgnnass  13493  mulgnn0ass  13494  mulgass  13495  mulgassr  13496  mulgmodid  13497  mulgsubdir  13498  submmulg  13502  isnsg3  13543  nmzsubg  13546  ssnmz  13547  0nsg  13550  eqger  13560  eqgid  13562  eqgcpbl  13564  ghmlin  13584  ghmmulg  13592  ghmnsgima  13604  ghmnsgpreima  13605  conjghm  13612  conjnmz  13615  ablsub2inv  13647  abladdsub4  13650  abladdsub  13651  ablpncan2  13652  ablpnpcan  13656  ablnncan  13657  ablnnncan1  13660  gsumfzconst  13677  gsumfzsnfd  13681  mgpress  13693  rngass  13701  rngdi  13702  rngdir  13703  rnglz  13707  rngmneg1  13709  rngsubdir  13714  rngpropd  13717  imasrng  13718  srgass  13733  srgmulgass  13751  srgpcomp  13752  srgpcompp  13753  srgpcomppsc  13754  ringpropd  13800  ringlz  13805  ring1eq0  13810  ringnegl  13813  ringmneg1  13815  ringsubdir  13819  mulgass2  13820  ring1  13821  imasring  13826  opprrng  13839  opprring  13841  unitgrp  13878  dvrcan1  13902  rdivmuldivd  13906  subrginv  13999  resrhm  14010  unitrrg  14029  islmod  14053  lmodlema  14054  islmodd  14055  lmod0vs  14083  lmodvs0  14084  lmodvsmmulgdi  14085  lmodvneg1  14092  lmodvsneg  14093  lmodsubvs  14105  lmodsubdi  14106  lmodsubdir  14107  lmodprop2d  14110  rmodislmodlem  14112  rmodislmod  14113  lsssetm  14118  islssmd  14121  lssclg  14126  lssvacl  14127  lss1d  14145  lsspropdg  14193  sraval  14199  rnglidlmcl  14242  gsumfzfsumlemm  14349  znunit  14421  mplsubgfilemcl  14461  resttop  14642  restco  14646  restin  14648  lmfval  14664  cnprcl2k  14678  txrest  14748  txdis1cn  14750  cnmpt2res  14769  psmettri2  14800  psmettri  14802  xmettri2  14833  xmettri  14844  mettri  14845  metrtri  14849  blvalps  14860  blval  14861  xblss2  14877  blhalf  14880  comet  14971  xmetxp  14979  txmetcnp  14990  cnmet  15002  ioo2bl  15023  ivthreinc  15117  limcmpted  15135  limcimolemlt  15136  cnplimclemr  15141  limccnp2cntop  15149  reldvg  15151  dvfvalap  15153  dvidlemap  15163  dvidrelem  15164  dvidsslem  15165  dvconst  15166  dvconstre  15168  dvconstss  15170  dvcnp2cntop  15171  dvaddxxbr  15173  dvmulxxbr  15174  dvcoapbr  15179  dvcjbr  15180  dvexp  15183  dvrecap  15185  dvmptcmulcn  15193  dveflem  15198  plyval  15204  elply2  15207  elplyr  15212  elplyd  15213  ply1termlem  15214  plyaddlem1  15219  plymullem1  15220  plycoeid3  15229  plycjlemc  15232  dvply1  15237  sin0pilem1  15253  sinperlem  15280  ptolemy  15296  tangtx  15310  abssinper  15318  reexplog  15343  relogexp  15344  cxprec  15382  rpdivcxp  15383  cxpmul  15384  rpabscxpbnd  15412  rplogbval  15417  rplogbreexp  15425  rprelogbmul  15427  logbrec  15432  logbgcd1irraplemap  15441  binom4  15451  wilthlem1  15452  mpodvdsmulf1o  15462  sgmppw  15464  0sgmppw  15465  1sgmprm  15466  1sgm2ppw  15467  perfectlem1  15471  perfectlem2  15472  perfect  15473  lgslem1  15477  lgslem4  15480  lgsval  15481  lgsfvalg  15482  lgsval2lem  15487  lgsval4lem  15488  lgsvalmod  15496  lgsneg  15501  lgsneg1  15502  lgsmod  15503  lgsdilem  15504  lgsdir2lem4  15508  lgsdir2  15510  lgsdirprm  15511  lgsdir  15512  lgsne0  15515  lgssq  15517  lgssq2  15518  lgsmulsqcoprm  15523  lgsdirnn0  15524  lgsdinn0  15525  gausslemma2dlem1a  15535  gausslemma2dlem4  15541  gausslemma2dlem5a  15542  gausslemma2dlem5  15543  gausslemma2dlem6  15544  gausslemma2dlem7  15545  gausslemma2d  15546  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisenlem4  15550  lgseisen  15551  lgsquadlem1  15554  lgsquadlem2  15555  lgsquad2lem1  15558  lgsquad2lem2  15559  lgsquad3  15561  m1lgs  15562  2lgslem1a  15565  2lgslem1c  15567  2lgslem3a  15570  2lgslem3b  15571  2lgslem3c  15572  2lgslem3d  15573  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577  2lgsoddprmlem1  15582  2lgsoddprmlem2  15583  2lgsoddprmlem3  15588  2sqlem1  15591  2sqlem2  15592  mul2sq  15593  2sqlem3  15594  2sqlem4  15595  2sqlem8  15600  2sqlem9  15601  2sqlem10  15602  trilpolemeq1  15979  trilpolemlt1  15980  trirec0xor  15984  apdifflemf  15985  apdiff  15987