Theorem oveq1d 6100

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402  (class class class)co 6085

This proof depends on 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 proof 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 3715  df-pr 3716  df-op 3718  df-uni 3936  df-br 4131  df-iota 5337  df-fv 5385  df-ov 6088

This theorem is used by:  fvoveq1d  6107  csbov2g  6127  caovassg  6248  caovdig  6264  caovdirg  6267  caov12d  6271  caov31d  6272  caov411d  6275  caofinvl  6328  suppofss1dcl  6504  suppofss2dcl  6505  omsuc  6745  nnmsucr  6761  nnm1  6798  nnm2  6799  ecovass  6918  ecoviass  6919  ecovdi  6920  ecovidi  6921  isacnm  7560  addasspig  7698  mulasspig  7700  mulpipq2  7739  distrnqg  7755  ltsonq  7766  ltanqg  7768  ltmnqg  7769  ltexnqq  7776  archnqq  7785  prarloclemarch2  7787  enq0sym  7800  addnq0mo  7815  mulnq0mo  7816  addnnnq0  7817  nqpnq0nq  7821  nq0m0r  7824  nq0a0  7825  nnanq0  7826  distrnq0  7827  addassnq0  7830  addpinq1  7832  prarloclemlo  7862  prarloclem3  7865  prarloclem5  7868  prarloclemcalc  7870  addnqprllem  7895  addnqprulem  7896  appdivnq  7931  recexprlem1ssl  8001  recexprlem1ssu  8002  ltmprr  8010  cauappcvgprlemladdru  8024  cauappcvgprlem1  8027  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemcl  8044  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprlem1  8047  caucvgprprlemcbv  8055  caucvgprprlemval  8056  caucvgprprlemexb  8075  caucvgprprlem1  8077  addcmpblnr  8107  mulcmpblnrlemg  8108  addsrmo  8111  mulsrmo  8112  addsrpr  8113  mulsrpr  8114  ltsrprg  8115  1idsr  8136  pn0sr  8139  recexgt0sr  8141  mulgt0sr  8146  srpospr  8151  prsradd  8154  caucvgsrlemfv  8159  caucvgsrlemcau  8161  caucvgsrlemgt1  8163  caucvgsrlemoffval  8164  caucvgsrlemoffcau  8166  caucvgsrlemoffres  8168  caucvgsrlembnd  8169  caucvgsr  8170  map2psrprg  8173  pitonnlem1p1  8214  pitonnlem2  8215  pitonn  8216  recidpirqlemcalc  8225  ax1rid  8245  axrnegex  8247  axcnre  8249  recriota  8258  nntopi  8262  axcaucvglemval  8265  axcaucvglemcau  8266  axcaucvglemres  8267  mul12  8457  mul4  8460  muladd11  8461  readdcan  8468  muladd11r  8484  add12  8486  cnegex  8506  addcan  8508  negeu  8519  pncan2  8535  addsubass  8538  addsub  8539  2addsub  8542  addsubeq4  8543  subid  8547  subid1  8548  npncan  8549  nppcan  8550  nnpcan  8551  nnncan1  8564  npncan3  8566  pnpcan  8567  pnncan  8569  ppncan  8570  addsub4  8571  negsub  8576  subneg  8577  subeqxfrd  8691  mvlraddd  8692  mvlladdd  8693  mvrraddd  8694  subaddeqd  8697  ine0  8723  mulneg1  8724  ltadd2  8749  apreap  8918  cru  8933  recexap  8984  mulcanapd  8992  div23ap  9024  div13ap  9026  divmulassap  9028  divmulasscomap  9029  divcanap4  9032  muldivdirap  9040  divsubdirap  9041  divmuldivap  9045  divdivdivap  9046  divcanap5  9047  divmul13ap  9048  divmuleqap  9050  divdiv32ap  9053  divcanap7  9054  dmdcanap  9055  divdivap1  9056  divdivap2  9057  divadddivap  9060  divsubdivap  9061  conjmulap  9062  divneg2ap  9069  subrecap  9172  mvllmulapd  9175  lt2mul2div  9212  nndivtr  9349  2halves  9539  halfaddsub  9544  subhalfhalf  9545  avgle1  9551  avgle2  9552  div4p1lem1div2  9564  un0addcl  9601  un0mulcl  9602  peano2z  9685  zneo  9752  nneoor  9753  nneo  9754  zeo  9756  zeo2  9757  deceq1  9786  qreccl  10052  xaddcom  10274  xnegdi  10281  xaddass  10282  xaddass2  10283  xpncan  10284  xleadd1a  10286  xltadd1  10289  xposdif  10295  xadd4d  10298  lincmb01cmp  10416  lincmble  10417  iccf1o  10418  fzspl  10487  fz0to4untppr  10542  fzo0addel  10617  fzosubel3  10625  qavgle  10704  2tnp1ge0ge0  10751  fldiv4p1lem1div2  10755  fldiv4lem1div2  10757  ceilqm1lt  10764  flqdiv  10773  modqlt  10785  modqdiffl  10787  modqcyc2  10812  modqaddabs  10814  mulqaddmodid  10816  mulp1mod1  10817  modqmuladd  10818  modqmuladdnn0  10820  qnegmod  10821  addmodid  10824  addmodidr  10825  modqadd2mod  10826  modqm1p1mod0  10827  modqmul12d  10830  modqnegd  10831  modqadd12d  10832  modqsub12d  10833  q2submod  10837  modqmulmodr  10842  modqaddmulmod  10843  modqsubdir  10845  modfzo0difsn  10847  modsumfzodifsn  10848  addmodlteq  10850  frecuzrdgsuc  10866  frecfzennn  10878  iseqovex  10910  seq3-1p  10942  seq3caopr2  10945  seqcaopr2g  10946  seq3caopr  10947  seqcaoprg  10948  seqf1oglem2a  10970  seqf1oglem1  10971  seqf1oglem2  10972  seq3id  10977  seq3homo  10979  seq3z  10980  seqhomog  10982  seqfeq4g  10983  expp1  10998  exprecap  11032  expaddzaplem  11034  expmulzap  11037  expdivap  11042  sqval  11049  sqsubswap  11051  sqdividap  11056  subsq  11098  subsq2  11099  binom2  11103  binom2sub  11105  mulbinom2  11108  binom3  11109  zesq  11111  bernneq2  11114  modqexp  11119  sqoddm1div8  11146  mulsubdivbinom2ap  11165  nn0opthlem1d  11174  nn0opthd  11176  nn0opth2d  11177  facp1  11184  facdiv  11192  facndiv  11193  faclbnd  11195  faclbnd2  11196  faclbnd3  11197  bcval  11203  bccmpl  11208  bcm1k  11214  bcp1n  11215  bcp1nk  11216  bcval5  11217  bcp1m1  11219  bcpasc  11220  bcm1n  11223  bcn2m1  11224  hashprg  11265  hashdifpr  11277  hashfzo  11279  hashfzp1  11281  hashfz0  11282  hashxp  11283  hashfibclem  11298  hashfibc  11299  hashf1  11303  zfz1isolemsplit  11306  zfz1isolem1  11308  seq3coll  11310  lswwrd  11367  ccatfvalfi  11376  ccatass  11392  lswccatn0lsw  11395  wrdlenccats1lenm1g  11420  ccatw2s1leng  11422  ccatswrd  11458  ccatpfx  11489  swrdpfx  11495  pfxpfx  11496  ccats1pfxeq  11502  wrdeqs1cat  11508  wrdind  11510  wrd2ind  11511  pfxccatpfx2  11525  pfxccatin12d  11533  cats1catd  11556  cats2catd  11557  s2leng  11577  s3s4d  11591  s2s5d  11592  s5s2d  11593  reval  11630  crre  11638  remim  11641  remul2  11654  immul2  11661  imval2  11675  sq01  11676  cjdivap  11691  caucvgre  11763  cvg1nlemcau  11766  cvg1nlemres  11767  resqrexlemp1rp  11788  resqrexlemfp1  11791  resqrexlemover  11792  resqrexlemcalc1  11796  resqrexlemcalc3  11798  resqrexlemnm  11800  resqrexlemoverl  11803  resqrexlemglsq  11804  resqrexlemga  11805  resqrexlemsqa  11806  resqrexlemex  11807  resqrex  11808  sqrtdiv  11824  absvalsq  11835  absreimsq  11849  absdivap  11852  cau3lem  11897  maxabslemlub  11990  maxabslemval  11991  max0addsup  12002  minabs  12020  bdtrilem  12024  bdtri  12025  xrmaxaddlem  12045  xrmaxadd  12046  xrbdtri  12061  clim  12066  clim2  12068  climshftlemg  12087  climshft2  12091  climcn1  12093  climcn2  12094  subcn2  12096  reccn2ap  12098  climmulc2  12116  climsubc2  12118  clim2ser  12122  iser3shft  12131  climcau  12132  serf0  12137  fzosump1  12203  fsum1p  12204  fsump1  12206  sumsplitdc  12218  fsump1i  12219  mptfzshft  12228  fisum0diag2  12233  fsumconst  12240  fsumdifsnconst  12241  modfsummodlemstep  12243  modfsummod  12244  telfsumo  12252  fsumparts  12256  fsumrelem  12257  hash2iun1dif1  12266  binomlem  12269  binom  12270  binom1p  12271  binom1dif  12273  bcxmas  12275  isumsplit  12277  isum1p  12278  arisum  12284  arisum2  12285  trireciplem  12286  geoserap  12293  geolim  12297  geolim2  12298  georeclim  12299  geo2sum  12300  geoisum1  12305  cvgratnnlemseq  12312  cvgratnnlemsumlt  12314  cvgratnnlemfm  12315  cvgratz  12318  mertenslemi1  12321  mertenslem2  12322  mertensabs  12323  fprod1p  12385  fprodp1  12386  fprodcl2lem  12391  fprodfac  12401  fprodeq0  12403  fprodconst  12406  fprodrec  12415  fprodsplit1f  12420  fprodmodd  12427  efcllemp  12444  ef0lem  12446  efval  12447  esum  12448  ege2le3  12457  efaddlem  12460  efsep  12477  effsumlt  12478  eft0val  12479  efgt1p2  12481  efgt1p  12482  sinval  12488  cosval  12489  resinval  12501  recosval  12502  efi4p  12503  resin4p  12504  recos4p  12505  sinneg  12512  cosneg  12513  efival  12518  sinadd  12522  cosadd  12523  tanaddap  12525  sinmul  12530  cosmul  12531  cos2t  12536  cos2tsin  12537  ef01bndlem  12542  absefib  12557  demoivre  12559  demoivreALT  12560  eirraplem  12563  p1modz1  12580  dvdsmodexp  12581  moddvds  12585  mulmoddvds  12649  3dvds2dec  12652  zeo3  12654  odd2np1lem  12658  odd2np1  12659  oexpneg  12663  2tp1odd  12670  ltoddhalfle  12679  opoe  12681  opeo  12683  omeo  12684  m1expo  12686  m1exp1  12687  nn0o1gt2  12691  nn0o  12693  divalglemnn  12704  divalglemqt  12705  divalglemeunn  12707  divalglemex  12708  divalglemeuneg  12709  flodddiv4  12722  flodddiv4t2lthalf  12725  bitsp1o  12739  bitsmod  12742  bitsinv1lem  12747  gcdaddm  12780  bezoutlemnewy  12792  bezoutlema  12795  bezoutlemb  12796  bezoutlemex  12797  bezoutlemaz  12799  mulgcd  12812  gcddiv  12815  gcdmultiplez  12817  rpmulgcd  12822  rplpwr  12823  uzwodc  12833  lcmgcdlem  12874  lcmgcd  12875  divgcdcoprmex  12899  cncongr2  12901  prmexpb  12949  rpexp  12951  rpexp1i  12952  sqrt2irrlem  12959  nnmaxpwlemxy  12967  nnmaxpwlemndvds  12969  sqpweven  12974  2sqpwodd  12975  sqne2sq  12976  qmuldeneqnum  12994  nn0gcdsq  12999  zgcdsq  13000  numdensq  13001  dfphi2  13021  phiprmpw  13023  phiprm  13024  eulerthlema  13031  eulerthlemh  13032  eulerthlemth  13033  fermltl  13035  prmdiv  13036  prmdiveq  13037  prmdivdiv  13038  hashgcdlem  13039  odzval  13043  odzcllem  13044  odzdvds  13047  vfermltl  13053  powm2modprm  13054  reumodprminv  13055  modprm0  13056  nnnn0modprm0  13057  modprmn0modprm0  13058  coprimeprodsq  13059  coprimeprodsq2  13060  pythagtriplem1  13067  pythagtriplem3  13069  pythagtriplem4  13070  pythagtriplem6  13072  pythagtriplem7  13073  pythagtriplem12  13077  pythagtriplem14  13079  pythagtriplem15  13080  pythagtriplem16  13081  pythagtriplem17  13082  pythagtriplem18  13083  pceu  13097  pczpre  13099  pcdiv  13104  pcqdiv  13109  pcrec  13110  pczndvds  13118  pcneg  13127  pc2dvds  13132  pcprmpw2  13135  pcaddlem  13141  pcadd  13142  fldivp1  13150  pockthlem  13158  pockthi  13160  4sqlem5  13184  4sqlem9  13188  4sqlem10  13189  4sqlem2  13191  4sqlem3  13192  4sqlem4  13194  mul4sqlem  13195  4sqlem11  13203  4sqlem12  13204  4sqlem14  13206  4sqlem15  13207  4sqlem17  13209  4sqlem19  13211  ballotfilem2  13280  ballotfilemfp1  13283  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilem4  13293  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemsval  13304  ballotfilemsdom  13307  ballotfilemsima  13311  ballotfilemieq  13312  ballotfilemfrci  13323  ballotfilemth  13333  ballotfi  13334  ennnfonelemkh  13355  ennnfonelemhf1o  13356  setscomd  13445  ressressg  13482  qusex  13699  qusin  13700  grpinvalem  13758  grpinva  13759  grprida  13760  gzsumsplit1r  13768  isnsgrp  13774  sgrpass  13776  sgrp1  13779  sgrppropd  13781  mnd12g  13794  mndpropd  13806  imasmnd2  13812  mhmex  13822  mhmlin  13827  grprcan  13895  grpinvid1  13910  isgrpinv  13912  grplcan  13920  grpasscan1  13921  grplmulf1o  13932  grpinvadd  13936  grpinvsub  13940  grpsubsub4  13951  grppnpcan2  13952  grpnpncan  13953  dfgrp3mlem  13956  dfgrp3m  13957  grplactcnv  13960  imasgrp2  13966  mhmlem  13970  mhmid  13971  mhmmnd  13972  mulgnnp1  13986  mulg2  13987  mulgnn0p1  13989  mulgsubcl  13992  mulgneg  13996  mulgaddcomlem  14001  mulgaddcom  14002  mulgz  14006  mulgnn0dir  14008  mulgdirlem  14009  mulgdir  14010  mulgneg2  14012  mulgnnass  14013  mulgnn0ass  14014  mulgass  14015  mulgassr  14016  mulgmodid  14017  mulgsubdir  14018  submmulg  14022  isnsg3  14063  nmzsubg  14066  ssnmz  14067  0nsg  14070  eqger  14080  eqgid  14082  eqgcpbl  14084  ghmlin  14104  ghmmulg  14112  ghmnsgima  14124  ghmnsgpreima  14125  conjghm  14132  conjnmz  14135  cntzsgrpcl  14161  cntzsubm  14164  cntzsubg  14165  cntrsubgnsg  14169  ablsub2inv  14199  abladdsub4  14202  abladdsub  14203  ablpncan2  14204  ablpnpcan  14208  ablnncan  14209  ablnnncan1  14212  gzsumconst  14227  gzsumsnfd  14231  gzsumsplit0  14232  gzsumshift  14233  gzsumgsum  14239  gsummptfidmadd  14245  gsumconstcmn  14250  prdssgrpd  14275  prdsidlem  14277  prdsmndd  14278  prdsinvlem  14280  mgpress  14314  rngass  14322  rngdi  14323  rngdir  14324  rnglz  14328  rngmneg1  14330  rngsubdir  14335  rngpropd  14338  imasrng  14339  srgass  14359  srgmulgass  14377  srgpcomp  14378  srgpcompp  14379  srgpcomppsc  14380  ringpropd  14427  ringlz  14432  ring1eq0  14437  ringnegl  14440  ringmneg1  14442  ringsubdir  14446  mulgass2  14447  ring1  14448  imasring  14453  opprrng  14466  opprring  14468  unitgrp  14507  dvrcan1  14531  rdivmuldivd  14535  subrginv  14629  resrhm  14640  unitrrg  14660  aprlring  14684  islmod  14711  lmodlema  14712  islmodd  14713  lmod0vs  14742  lmodvs0  14743  lmodvsmmulgdi  14744  lmodvneg1  14751  lmodvsneg  14752  lmodsubvs  14764  lmodsubdi  14765  lmodsubdir  14766  lmodprop2d  14769  rmodislmodlem  14771  rmodislmod  14772  lsssetm  14777  islssmd  14780  lssclg  14785  lssvacl  14786  lss1d  14804  lsspropdg  14852  sraval  14858  rnglidlmcl  14901  znunit  15078  isassa  15086  assalem  15087  assa2ass  15093  assapropd  15098  asclmul1  15113  assamulgscmlem2  15126  mplsubgfilemcl  15181  resttop  15362  restco  15366  restin  15368  lmfval  15385  cnprcl2k  15398  txrest  15468  txdis1cn  15470  cnmpt2res  15489  psmettri2  15520  psmettri  15522  xmettri2  15553  xmettri  15564  mettri  15565  metrtri  15569  blvalps  15580  blval  15581  xblss2  15597  blhalf  15600  comet  15691  xmetxp  15699  txmetcnp  15710  cnmet  15722  ioo2bl  15743  ivthreinc  15837  limcmpted  15855  limcimolemlt  15856  cnplimclemr  15861  limccnp2cntop  15869  reldvg  15871  dvfvalap  15873  dvidlemap  15883  dvidrelem  15884  dvidsslem  15885  dvconst  15886  dvconstre  15888  dvconstss  15890  dvcnp2cntop  15891  dvaddxxbr  15893  dvmulxxbr  15894  dvcoapbr  15899  dvcjbr  15900  dvexp  15903  dvrecap  15905  dvmptcmulcn  15913  dveflem  15918  plyval  15924  elply2  15927  elplyr  15932  elplyd  15933  ply1termlem  15934  plyaddlem1  15939  plymullem1  15940  plycoeid3  15949  plycjlemc  15952  dvply1  15957  sin0pilem1  15974  sinperlem  16001  ptolemy  16017  tangtx  16031  abssinper  16039  reexplog  16065  relogexp  16066  cxprec  16107  rpdivcxp  16108  cxpmul  16109  rpabscxpbnd  16137  rplogbval  16142  rplogbreexp  16150  rprelogbmul  16152  logbrec  16157  logbgcd1irraplemap  16166  zprmlogbaplem1  16176  zprmlogbaplem3  16178  zprmlogbap  16179  binom4  16180  log2tlbndlog2  16181  log2ublem2  16183  birthdaylem2  16187  birthdaylem3  16188  pellexlem2  16191  pellexlem3  16192  wilthlem1  16193  ppiprm  16220  ppiqp1le  16228  mpodvdsmulf1o  16245  sgmppw  16247  0sgmppw  16248  1sgmprm  16249  1sgm2ppw  16250  ppiqub  16254  chtqleppi  16255  chtublem  16256  chtqub  16257  perfectlem1  16260  perfectlem2  16261  perfect  16262  bcctr  16263  pcbcctr  16264  bcmono  16265  bcp1ctr  16267  bclbnd  16268  bposlem3  16274  bposlem6  16277  bposlem9  16280  lgslem1  16285  lgslem4  16288  lgsval  16289  lgsfvalg  16290  lgsval2lem  16295  lgsval4lem  16296  lgsvalmod  16304  lgsneg  16309  lgsneg1  16310  lgsmod  16311  lgsdilem  16312  lgsdir2lem4  16316  lgsdir2  16318  lgsdirprm  16319  lgsdir  16320  lgsne0  16323  lgssq  16325  lgssq2  16326  lgsmulsqcoprm  16331  lgsdirnn0  16332  lgsdinn0  16333  gausslemma2dlem1a  16343  gausslemma2dlem4  16349  gausslemma2dlem5a  16350  gausslemma2dlem5  16351  gausslemma2dlem6  16352  gausslemma2dlem7  16353  gausslemma2d  16354  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisenlem4  16358  lgseisen  16359  lgsquadlem1  16362  lgsquadlem2  16363  lgsquad2lem1  16366  lgsquad2lem2  16367  lgsquad3  16369  m1lgs  16370  2lgslem1a  16373  2lgslem1c  16375  2lgslem3a  16378  2lgslem3b  16379  2lgslem3c  16380  2lgslem3d  16381  2lgslem3a1  16382  2lgslem3b1  16383  2lgslem3c1  16384  2lgslem3d1  16385  2lgsoddprmlem1  16390  2lgsoddprmlem2  16391  2lgsoddprmlem3  16396  2sqlem1  16399  2sqlem2  16400  mul2sq  16401  2sqlem3  16402  2sqlem4  16403  2sqlem8  16408  2sqlem9  16409  2sqlem10  16410  vdegp1bid  16722  uspgr2wlkeqi  16774  isclwwlk  16801  clwwlkccatlem  16807  clwwlknonex2  16846  repiecele0  17241  repiecege0  17242  repiecef  17243  trilpolemeq1  17256  trilpolemlt1  17257  trirec0xor  17261  apdifflemf  17262  apdiff  17264  qdiff  17265