Theorem oveq1d 5937

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

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

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 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925

This theorem is referenced by:  fvoveq1d  5944  csbov2g  5963  caovassg  6082  caovdig  6098  caovdirg  6101  caov12d  6105  caov31d  6106  caov411d  6109  caofinvl  6160  omsuc  6530  nnmsucr  6546  nnm1  6583  nnm2  6584  ecovass  6703  ecoviass  6704  ecovdi  6705  ecovidi  6706  addasspig  7397  mulasspig  7399  mulpipq2  7438  distrnqg  7454  ltsonq  7465  ltanqg  7467  ltmnqg  7468  ltexnqq  7475  archnqq  7484  prarloclemarch2  7486  enq0sym  7499  addnq0mo  7514  mulnq0mo  7515  addnnnq0  7516  nqpnq0nq  7520  nq0m0r  7523  nq0a0  7524  nnanq0  7525  distrnq0  7526  addassnq0  7529  addpinq1  7531  prarloclemlo  7561  prarloclem3  7564  prarloclem5  7567  prarloclemcalc  7569  addnqprllem  7594  addnqprulem  7595  appdivnq  7630  recexprlem1ssl  7700  recexprlem1ssu  7701  ltmprr  7709  cauappcvgprlemladdru  7723  cauappcvgprlem1  7726  caucvgprlemnkj  7733  caucvgprlemnbj  7734  caucvgprlemcl  7743  caucvgprlemladdfu  7744  caucvgprlemladdrl  7745  caucvgprlem1  7746  caucvgprprlemcbv  7754  caucvgprprlemval  7755  caucvgprprlemexb  7774  caucvgprprlem1  7776  addcmpblnr  7806  mulcmpblnrlemg  7807  addsrmo  7810  mulsrmo  7811  addsrpr  7812  mulsrpr  7813  ltsrprg  7814  1idsr  7835  pn0sr  7838  recexgt0sr  7840  mulgt0sr  7845  srpospr  7850  prsradd  7853  caucvgsrlemfv  7858  caucvgsrlemcau  7860  caucvgsrlemgt1  7862  caucvgsrlemoffval  7863  caucvgsrlemoffcau  7865  caucvgsrlemoffres  7867  caucvgsrlembnd  7868  caucvgsr  7869  map2psrprg  7872  pitonnlem1p1  7913  pitonnlem2  7914  pitonn  7915  recidpirqlemcalc  7924  ax1rid  7944  axrnegex  7946  axcnre  7948  recriota  7957  nntopi  7961  axcaucvglemval  7964  axcaucvglemcau  7965  axcaucvglemres  7966  mul12  8155  mul4  8158  muladd11  8159  readdcan  8166  muladd11r  8182  add12  8184  cnegex  8204  addcan  8206  negeu  8217  pncan2  8233  addsubass  8236  addsub  8237  2addsub  8240  addsubeq4  8241  subid  8245  subid1  8246  npncan  8247  nppcan  8248  nnpcan  8249  nnncan1  8262  npncan3  8264  pnpcan  8265  pnncan  8267  ppncan  8268  addsub4  8269  negsub  8274  subneg  8275  subeqxfrd  8389  mvlraddd  8390  mvlladdd  8391  mvrraddd  8392  subaddeqd  8395  ine0  8420  mulneg1  8421  ltadd2  8446  apreap  8614  cru  8629  recexap  8680  mulcanapd  8688  div23ap  8718  div13ap  8720  divmulassap  8722  divmulasscomap  8723  divcanap4  8726  muldivdirap  8734  divsubdirap  8735  divmuldivap  8739  divdivdivap  8740  divcanap5  8741  divmul13ap  8742  divmuleqap  8744  divdiv32ap  8747  divcanap7  8748  dmdcanap  8749  divdivap1  8750  divdivap2  8751  divadddivap  8754  divsubdivap  8755  conjmulap  8756  divneg2ap  8763  subrecap  8866  mvllmulapd  8869  lt2mul2div  8906  nndivtr  9032  2halves  9220  halfaddsub  9225  subhalfhalf  9226  avgle1  9232  avgle2  9233  div4p1lem1div2  9245  un0addcl  9282  un0mulcl  9283  peano2z  9362  zneo  9427  nneoor  9428  nneo  9429  zeo  9431  zeo2  9432  deceq1  9461  qreccl  9716  xaddcom  9936  xnegdi  9943  xaddass  9944  xaddass2  9945  xpncan  9946  xleadd1a  9948  xltadd1  9951  xposdif  9957  xadd4d  9960  lincmb01cmp  10078  iccf1o  10079  fz0to4untppr  10199  fzosubel3  10272  qavgle  10348  2tnp1ge0ge0  10391  fldiv4p1lem1div2  10395  fldiv4lem1div2  10397  ceilqm1lt  10404  flqdiv  10413  modqlt  10425  modqdiffl  10427  modqcyc2  10452  modqaddabs  10454  mulqaddmodid  10456  mulp1mod1  10457  modqmuladd  10458  modqmuladdnn0  10460  qnegmod  10461  addmodid  10464  addmodidr  10465  modqadd2mod  10466  modqm1p1mod0  10467  modqmul12d  10470  modqnegd  10471  modqadd12d  10472  modqsub12d  10473  q2submod  10477  modqmulmodr  10482  modqaddmulmod  10483  modqsubdir  10485  modfzo0difsn  10487  modsumfzodifsn  10488  addmodlteq  10490  frecuzrdgsuc  10506  frecfzennn  10518  iseqovex  10550  seq3-1p  10582  seq3caopr2  10585  seqcaopr2g  10586  seq3caopr  10587  seqcaoprg  10588  seqf1oglem2a  10610  seqf1oglem1  10611  seqf1oglem2  10612  seq3id  10617  seq3homo  10619  seq3z  10620  seqhomog  10622  seqfeq4g  10623  expp1  10638  exprecap  10672  expaddzaplem  10674  expmulzap  10677  expdivap  10682  sqval  10689  sqsubswap  10691  sqdividap  10696  subsq  10738  subsq2  10739  binom2  10743  binom2sub  10745  mulbinom2  10748  binom3  10749  zesq  10750  bernneq2  10753  modqexp  10758  sqoddm1div8  10785  mulsubdivbinom2ap  10803  nn0opthlem1d  10812  nn0opthd  10814  nn0opth2d  10815  facp1  10822  facdiv  10830  facndiv  10831  faclbnd  10833  faclbnd2  10834  faclbnd3  10835  bcval  10841  bccmpl  10846  bcm1k  10852  bcp1n  10853  bcp1nk  10854  bcval5  10855  bcp1m1  10857  bcpasc  10858  bcn2m1  10861  hashprg  10900  hashdifpr  10912  hashfzo  10914  hashfzp1  10916  hashfz0  10917  hashxp  10918  zfz1isolemsplit  10930  zfz1isolem1  10932  seq3coll  10934  reval  11014  crre  11022  remim  11025  remul2  11038  immul2  11045  imval2  11059  cjdivap  11074  caucvgre  11146  cvg1nlemcau  11149  cvg1nlemres  11150  resqrexlemp1rp  11171  resqrexlemfp1  11174  resqrexlemover  11175  resqrexlemcalc1  11179  resqrexlemcalc3  11181  resqrexlemnm  11183  resqrexlemoverl  11186  resqrexlemglsq  11187  resqrexlemga  11188  resqrexlemsqa  11189  resqrexlemex  11190  resqrex  11191  sqrtdiv  11207  absvalsq  11218  absreimsq  11232  absdivap  11235  cau3lem  11279  maxabslemlub  11372  maxabslemval  11373  max0addsup  11384  minabs  11401  bdtrilem  11404  bdtri  11405  xrmaxaddlem  11425  xrmaxadd  11426  xrbdtri  11441  clim  11446  clim2  11448  climshftlemg  11467  climshft2  11471  climcn1  11473  climcn2  11474  subcn2  11476  reccn2ap  11478  climmulc2  11496  climsubc2  11498  clim2ser  11502  iser3shft  11511  climcau  11512  serf0  11517  fzosump1  11582  fsum1p  11583  fsump1  11585  sumsplitdc  11597  fsump1i  11598  mptfzshft  11607  fisum0diag2  11612  fsumconst  11619  fsumdifsnconst  11620  modfsummodlemstep  11622  modfsummod  11623  telfsumo  11631  fsumparts  11635  fsumrelem  11636  hash2iun1dif1  11645  binomlem  11648  binom  11649  binom1p  11650  binom1dif  11652  bcxmas  11654  isumsplit  11656  isum1p  11657  arisum  11663  arisum2  11664  trireciplem  11665  geoserap  11672  geolim  11676  geolim2  11677  georeclim  11678  geo2sum  11679  geoisum1  11684  cvgratnnlemseq  11691  cvgratnnlemsumlt  11693  cvgratnnlemfm  11694  cvgratz  11697  mertenslemi1  11700  mertenslem2  11701  mertensabs  11702  fprod1p  11764  fprodp1  11765  fprodcl2lem  11770  fprodfac  11780  fprodeq0  11782  fprodconst  11785  fprodrec  11794  fprodsplit1f  11799  fprodmodd  11806  efcllemp  11823  ef0lem  11825  efval  11826  esum  11827  ege2le3  11836  efaddlem  11839  efsep  11856  effsumlt  11857  eft0val  11858  efgt1p2  11860  efgt1p  11861  sinval  11867  cosval  11868  resinval  11880  recosval  11881  efi4p  11882  resin4p  11883  recos4p  11884  sinneg  11891  cosneg  11892  efival  11897  sinadd  11901  cosadd  11902  tanaddap  11904  sinmul  11909  cosmul  11910  cos2t  11915  cos2tsin  11916  ef01bndlem  11921  absefib  11936  demoivre  11938  demoivreALT  11939  eirraplem  11942  p1modz1  11959  dvdsmodexp  11960  moddvds  11964  mulmoddvds  12028  3dvds2dec  12031  zeo3  12033  odd2np1lem  12037  odd2np1  12038  oexpneg  12042  2tp1odd  12049  ltoddhalfle  12058  opoe  12060  opeo  12062  omeo  12063  m1expo  12065  m1exp1  12066  nn0o1gt2  12070  nn0o  12072  divalglemnn  12083  divalglemqt  12084  divalglemeunn  12086  divalglemex  12087  divalglemeuneg  12088  flodddiv4  12101  flodddiv4t2lthalf  12104  bitsp1o  12117  gcdaddm  12151  bezoutlemnewy  12163  bezoutlema  12166  bezoutlemb  12167  bezoutlemex  12168  bezoutlemaz  12170  mulgcd  12183  gcddiv  12186  gcdmultiplez  12188  rpmulgcd  12193  rplpwr  12194  uzwodc  12204  lcmgcdlem  12245  lcmgcd  12246  divgcdcoprmex  12270  cncongr2  12272  prmexpb  12319  rpexp  12321  rpexp1i  12322  sqrt2irrlem  12329  oddpwdclemxy  12337  oddpwdclemndvds  12339  sqpweven  12343  2sqpwodd  12344  sqne2sq  12345  qmuldeneqnum  12363  nn0gcdsq  12368  zgcdsq  12369  numdensq  12370  dfphi2  12388  phiprmpw  12390  phiprm  12391  eulerthlema  12398  eulerthlemh  12399  eulerthlemth  12400  fermltl  12402  prmdiv  12403  prmdiveq  12404  prmdivdiv  12405  hashgcdlem  12406  odzval  12410  odzcllem  12411  odzdvds  12414  vfermltl  12420  powm2modprm  12421  reumodprminv  12422  modprm0  12423  nnnn0modprm0  12424  modprmn0modprm0  12425  coprimeprodsq  12426  coprimeprodsq2  12427  pythagtriplem1  12434  pythagtriplem3  12436  pythagtriplem4  12437  pythagtriplem6  12439  pythagtriplem7  12440  pythagtriplem12  12444  pythagtriplem14  12446  pythagtriplem15  12447  pythagtriplem16  12448  pythagtriplem17  12449  pythagtriplem18  12450  pceu  12464  pczpre  12466  pcdiv  12471  pcqdiv  12476  pcrec  12477  pczndvds  12485  pcneg  12494  pc2dvds  12499  pcprmpw2  12502  pcaddlem  12508  pcadd  12509  fldivp1  12517  pockthlem  12525  pockthi  12527  4sqlem5  12551  4sqlem9  12555  4sqlem10  12556  4sqlem2  12558  4sqlem3  12559  4sqlem4  12561  mul4sqlem  12562  4sqlem11  12570  4sqlem12  12571  4sqlem14  12573  4sqlem15  12574  4sqlem17  12576  4sqlem19  12578  ennnfonelemkh  12629  ennnfonelemhf1o  12630  setscomd  12719  ressressg  12753  qusex  12968  qusin  12969  grpinvalem  13028  grpinva  13029  grprida  13030  gsumsplit1r  13041  isnsgrp  13049  sgrpass  13051  sgrp1  13054  sgrppropd  13056  mnd12g  13069  mndpropd  13081  mhmex  13094  mhmlin  13099  grprcan  13169  grpinvid1  13184  isgrpinv  13186  grplcan  13194  grpasscan1  13195  grplmulf1o  13206  grpinvadd  13210  grpinvsub  13214  grpsubsub4  13225  grppnpcan2  13226  grpnpncan  13227  dfgrp3mlem  13230  dfgrp3m  13231  grplactcnv  13234  imasgrp2  13240  mhmlem  13244  mhmid  13245  mhmmnd  13246  mulgnnp1  13260  mulg2  13261  mulgnn0p1  13263  mulgsubcl  13266  mulgneg  13270  mulgaddcomlem  13275  mulgaddcom  13276  mulgz  13280  mulgnn0dir  13282  mulgdirlem  13283  mulgdir  13284  mulgneg2  13286  mulgnnass  13287  mulgnn0ass  13288  mulgass  13289  mulgassr  13290  mulgmodid  13291  mulgsubdir  13292  submmulg  13296  isnsg3  13337  nmzsubg  13340  ssnmz  13341  0nsg  13344  eqger  13354  eqgid  13356  eqgcpbl  13358  ghmlin  13378  ghmmulg  13386  ghmnsgima  13398  ghmnsgpreima  13399  conjghm  13406  conjnmz  13409  ablsub2inv  13441  abladdsub4  13444  abladdsub  13445  ablpncan2  13446  ablpnpcan  13450  ablnncan  13451  ablnnncan1  13454  gsumfzconst  13471  gsumfzsnfd  13475  mgpress  13487  rngass  13495  rngdi  13496  rngdir  13497  rnglz  13501  rngmneg1  13503  rngsubdir  13508  rngpropd  13511  imasrng  13512  srgass  13527  srgmulgass  13545  srgpcomp  13546  srgpcompp  13547  srgpcomppsc  13548  ringpropd  13594  ringlz  13599  ring1eq0  13604  ringnegl  13607  ringmneg1  13609  ringsubdir  13613  mulgass2  13614  ring1  13615  imasring  13620  opprrng  13633  opprring  13635  unitgrp  13672  dvrcan1  13696  rdivmuldivd  13700  subrginv  13793  resrhm  13804  unitrrg  13823  islmod  13847  lmodlema  13848  islmodd  13849  lmod0vs  13877  lmodvs0  13878  lmodvsmmulgdi  13879  lmodvneg1  13886  lmodvsneg  13887  lmodsubvs  13899  lmodsubdi  13900  lmodsubdir  13901  lmodprop2d  13904  rmodislmodlem  13906  rmodislmod  13907  lsssetm  13912  islssmd  13915  lssclg  13920  lssvacl  13921  lss1d  13939  lsspropdg  13987  sraval  13993  rnglidlmcl  14036  gsumfzfsumlemm  14143  znunit  14215  resttop  14406  restco  14410  restin  14412  lmfval  14428  cnprcl2k  14442  txrest  14512  txdis1cn  14514  cnmpt2res  14533  psmettri2  14564  psmettri  14566  xmettri2  14597  xmettri  14608  mettri  14609  metrtri  14613  blvalps  14624  blval  14625  xblss2  14641  blhalf  14644  comet  14735  xmetxp  14743  txmetcnp  14754  cnmet  14766  ioo2bl  14787  ivthreinc  14881  limcmpted  14899  limcimolemlt  14900  cnplimclemr  14905  limccnp2cntop  14913  reldvg  14915  dvfvalap  14917  dvidlemap  14927  dvidrelem  14928  dvidsslem  14929  dvconst  14930  dvconstre  14932  dvconstss  14934  dvcnp2cntop  14935  dvaddxxbr  14937  dvmulxxbr  14938  dvcoapbr  14943  dvcjbr  14944  dvexp  14947  dvrecap  14949  dvmptcmulcn  14957  dveflem  14962  plyval  14968  elply2  14971  elplyr  14976  elplyd  14977  ply1termlem  14978  plyaddlem1  14983  plymullem1  14984  plycoeid3  14993  plycjlemc  14996  dvply1  15001  sin0pilem1  15017  sinperlem  15044  ptolemy  15060  tangtx  15074  abssinper  15082  reexplog  15107  relogexp  15108  cxprec  15146  rpdivcxp  15147  cxpmul  15148  rpabscxpbnd  15176  rplogbval  15181  rplogbreexp  15189  rprelogbmul  15191  logbrec  15196  logbgcd1irraplemap  15205  binom4  15215  wilthlem1  15216  mpodvdsmulf1o  15226  sgmppw  15228  0sgmppw  15229  1sgmprm  15230  1sgm2ppw  15231  perfectlem1  15235  perfectlem2  15236  perfect  15237  lgslem1  15241  lgslem4  15244  lgsval  15245  lgsfvalg  15246  lgsval2lem  15251  lgsval4lem  15252  lgsvalmod  15260  lgsneg  15265  lgsneg1  15266  lgsmod  15267  lgsdilem  15268  lgsdir2lem4  15272  lgsdir2  15274  lgsdirprm  15275  lgsdir  15276  lgsne0  15279  lgssq  15281  lgssq2  15282  lgsmulsqcoprm  15287  lgsdirnn0  15288  lgsdinn0  15289  gausslemma2dlem1a  15299  gausslemma2dlem4  15305  gausslemma2dlem5a  15306  gausslemma2dlem5  15307  gausslemma2dlem6  15308  gausslemma2dlem7  15309  gausslemma2d  15310  lgseisenlem1  15311  lgseisenlem2  15312  lgseisenlem3  15313  lgseisenlem4  15314  lgseisen  15315  lgsquadlem1  15318  lgsquadlem2  15319  lgsquad2lem1  15322  lgsquad2lem2  15323  lgsquad3  15325  m1lgs  15326  2lgslem1a  15329  2lgslem1c  15331  2lgslem3a  15334  2lgslem3b  15335  2lgslem3c  15336  2lgslem3d  15337  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341  2lgsoddprmlem1  15346  2lgsoddprmlem2  15347  2lgsoddprmlem3  15352  2sqlem1  15355  2sqlem2  15356  mul2sq  15357  2sqlem3  15358  2sqlem4  15359  2sqlem8  15364  2sqlem9  15365  2sqlem10  15366  trilpolemeq1  15684  trilpolemlt1  15685  trirec0xor  15689  apdifflemf  15690  apdiff  15692