MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan9eq Structured version   Visualization version   GIF version

Theorem sylan9eq 2877
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
sylan9eq.1 (𝜑𝐴 = 𝐵)
sylan9eq.2 (𝜓𝐵 = 𝐶)
Assertion
Ref Expression
sylan9eq ((𝜑𝜓) → 𝐴 = 𝐶)

Proof of Theorem sylan9eq
StepHypRef Expression
1 sylan9eq.1 . 2 (𝜑𝐴 = 𝐵)
2 sylan9eq.2 . 2 (𝜓𝐵 = 𝐶)
3 eqtr 2842 . 2 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
41, 2, 3syl2an 598 1 ((𝜑𝜓) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2794
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2815
This theorem is referenced by:  sylan9req  2878  sylan9eqr  2879  difeq12  4069  uneq12  4109  ineq12  4158  ssdifim  4213  ifeq12  4456  ifbi  4460  ifeq12da  4471  preq12  4645  prprc  4677  opeq12  4780  opthwiener  5381  opthhausdorff0  5385  xpeq12  5557  sosn  5615  nfimad  5916  coi2  6094  funprg  6387  funtpg  6388  funcnvtp  6396  funcnvqp  6397  funimass1  6415  fimadmfoALT  6583  f1orescnv  6612  resdif  6617  fvmpt2  6761  fvmptnf  6772  fveqressseq  6829  oveq12  7149  cbvmpov  7233  ovmpog  7293  fvmpopr2d  7295  caofinvl  7421  eqopi  7711  el2mpocsbcl  7767  fmpoco  7777  mposn  7785  supp0cosupp0  7859  supp0cosupp0OLD  7860  imacosupp  7861  mpocurryd  7922  fvmpocurryd  7924  wrecseq123  7935  rdgsucmptf  8051  frsucmpt  8060  oevn0  8127  oa0r  8150  om1r  8156  oe1m  8158  omass  8193  oeoalem  8209  oeoa  8210  oeoe  8212  qseq12  8334  map0g  8435  xpcomco  8594  sbthlem4  8618  sbthlem5  8619  xpmapenlem  8672  phplem3  8686  phplem4  8687  unxpdomlem3  8712  funsnfsupp  8845  ordtypelem7  8976  cardennn  9400  dfac9  9551  alephsing  9687  axcc3  9849  ac6num  9890  konigthlem  9979  canthp1lem2  10064  ordpipq  10353  ltrnq  10390  addclprlem2  10428  mulclprlem  10430  prlem934  10444  prlem936  10458  mulcmpblnrlem  10481  addcnsr  10546  mulcnsr  10547  axcnre  10575  recex  11261  rpnnen1lem3  12366  rpnnen1lem5  12368  xaddpnf1  12607  xaddpnf2  12608  xaddmnf1  12609  xaddmnf2  12610  rexadd  12613  xnn0xaddcl  12616  xaddnemnf  12617  xaddnepnf  12618  xadddilem  12675  addmodlteq  13309  om2uzrani  13315  om2uzrdg  13319  seqf1olem2  13406  seqf1o  13407  modexp  13595  faclbnd4lem3  13651  hashunsng  13749  hashwrdn  13890  lsw1  13910  swrdfv  14001  swrdccat  14088  ccats1pfxeqbi  14095  revfv  14116  cshwsublen  14149  wrdlen2  14297  wrdl2exs2  14299  wwlktovf1  14312  relexp0  14373  relexpcnv  14385  shftcan1  14433  remul2  14480  immul2  14487  sumss  15072  geomulcvg  15223  fprodss  15293  binomfallfaclem2  15385  bpolylem  15393  ef0lem  15423  efieq1re  15543  rpnnen2lem1  15558  ruclem3  15577  dvdsnegb  15618  dvdscmul  15627  dvds2ln  15633  dvds2add  15634  dvds2sub  15635  gcdn0val  15836  rpmulgcd  15895  lcmn0val  15928  odzval  16117  pcval  16170  pcmpt  16217  prmreclem4  16244  1arithlem2  16249  vdwlem8  16313  ramcl2lem  16334  ramtcl  16335  ramtub  16337  ramcl2  16341  ramcl  16354  setsval  16504  prfcl  17444  curf1cl  17469  curfcl  17473  hofcl  17500  yonedalem4c  17518  psssdm  17817  grplactval  18192  mulgnn0gsum  18225  cntzval  18442  f1omvdco2  18567  pmtrfinv  18580  psgnunilem5  18613  odlem2  18658  gexlem2  18698  lsmvalx  18755  efgtval  18840  efgredlema  18857  vrgpval  18884  cyggex  19009  gsumcom2  19086  fincygsubgodd  19225  dvdsrtr  19396  abvtrivd  19602  lmhmco  19806  reslmhm  19815  lvecinv  19876  zrhmulg  20201  znzrhval  20236  ocvval  20354  mplmon2  20730  subrgasclcl  20736  coe1fv  20833  coe1fzgsumdlem  20928  evl1gsumdlem  20978  mat1dimscm  21078  dmatid  21098  scmatdmat  21118  mavmul0g  21156  1marepvmarrepid  21178  mdetunilem2  21216  gsummatr01lem3  21260  gsummatr01  21262  smadiadetlem3  21271  m2cpminvid2lem  21357  chpdmatlem2  21442  isopn3  21669  cnpval  21839  ptbasfi  22184  dfac14  22221  cnmptkk  22286  xkofvcn  22287  cnmptk1p  22288  cnmptk2  22289  xkocnv  22417  flfval  22593  ptcmplem3  22657  ptcmpg  22660  tmdmulg  22695  prdsxmslem2  23134  subgnm2  23238  nmoval  23319  fsum2cn  23474  pcovalg  23615  isclmp  23700  cphnm  23796  tcphnmval  23831  ovolctb  24092  ioorcl  24179  uniioombllem2  24185  itg1addlem3  24300  itg1climres  24316  itg2uba  24345  itg2splitlem  24350  elcpn  24535  dvexp  24554  dvexp2  24555  rolle  24591  cmvth  24592  mvth  24593  dvlip  24594  dvlipcn  24595  dvlip2  24596  dveq0  24601  dv11cn  24602  lhop1lem  24614  lhop2  24616  lhop  24617  dvcvx  24621  ftc2ditglem  24646  itgsubstlem  24649  ig1pval  24771  elply2  24791  coeid2  24834  coemul  24847  taylthlem2  24967  ulmdvlem1  24993  mtest  24997  pserval2  25004  abelthlem1  25024  abelthlem3  25026  abelthlem8  25032  abelthlem9  25033  pige3ALT  25110  0cxp  25255  leibpi  25526  igamgam  25632  mule1  25731  bposlem5  25870  lgsval3  25897  lgsdinn0  25927  dchrvmasumlem1  26077  dchrisum0flblem1  26090  rpvmasum2  26094  padicval  26199  axsegconlem1  26709  ax5seglem9  26729  axpasch  26733  axeuclidlem  26754  axcontlem2  26757  finsumvtxdg2ssteplem4  27336  usgr2wlkspthlem2  27545  crctcshlem4  27604  wwlknp  27627  wlkiswwlks2lem3  27655  wwlksnred  27676  wwlksnextproplem2  27694  umgrwwlks2on  27741  clwlkclwwlklem2a  27781  clwwisshclwwsn  27799  clwwlknlbonbgr1  27822  clwwlkn1loopb  27826  clwwlkf  27830  clwwlkext2edg  27839  wwlksext2clwwlk  27840  erclwwlknsym  27853  erclwwlkntr  27854  clwwlknon1  27880  clwwlknonex2  27892  eupth2lem3lem3  28013  eucrct2eupth  28028  fusgreghash2wspv  28118  2clwwlk2clwwlklem  28129  2clwwlk2clwwlk  28133  numclwwlk1lem2f1  28140  grpoidinvlem4  28288  grpoinvval  28304  grpodivval  28316  ipval  28484  sspgval  28510  sspsval  28512  sspnval  28518  nmooval  28544  ipasslem1  28612  ipasslem4  28615  hial0  28883  hial02  28884  ocsh  29064  pjhval  29178  hosval  29521  homval  29522  hodval  29523  hfsval  29524  hfmval  29525  braval  29725  kbval  29735  eigvalval  29741  0hmop  29764  adj0  29775  lnopeq0i  29788  nmopcoi  29876  pjclem4  29980  pj3si  29988  hstoh  30013  strlem3a  30033  hstrlem3a  30041  mdexchi  30116  atcv0eq  30160  atcv1  30161  fpwrelmap  30479  cycpmco2lem4  30802  cycpmco2lem5  30803  smatfval  31117  measxun2  31543  measdivcst  31557  measdivcstALTV  31558  ddeval1  31567  ddeval0  31568  ballotlemfp1  31823  signswmnd  31901  signstfvneq0  31916  signstfvc  31918  ftc2re  31943  itgexpif  31951  bnj1128  32336  subfacp1lem3  32503  subfacp1lem5  32505  cvmlift2lem3  32626  msubco  32852  altopthsn  33496  fnetr  33773  fnejoin2  33791  bj-evalid  34452  finxpreclem3  34771  finxpreclem5  34773  finxpreclem6  34774  curf  34993  curunc  34997  matunitlindf  35013  poimirlem4  35019  poimirlem25  35040  mblfinlem2  35053  mblfinlem3  35054  mbfresfi  35061  itg2addnclem  35066  itg2addnc  35069  ftc1anclem5  35092  isbnd3  35180  bndss  35182  grposnOLD  35278  ghomco  35287  xrneq12  35753  lkrval  36342  pmapval  37011  polvalN  37159  watvalN  37247  ldilset  37363  ltrnset  37372  dilsetN  37407  trnsetN  37410  trlset  37415  trlval  37416  cdleme16b  37533  cdleme31fv1  37645  cdlemg1idlemN  37826  tgrpset  37999  tendoset  38013  erngset  38054  erngplus  38057  erngmul  38060  erngset-rN  38062  erngplus-rN  38065  dvaset  38259  dvaplusg  38263  dvamulr  38266  dvavadd  38269  dvavsca  38271  diafval  38285  dvhset  38335  dvhmulr  38340  dvhvadd  38346  dvhvsca  38355  docafvalN  38376  djafvalN  38388  dibfval  38395  dicfval  38429  dihfval  38485  dihval  38486  dihvalc  38487  dihvalb  38491  dochfval  38604  djhfval  38651  lcdval  38843  mapdfval  38881  mapdn0  38923  hvmapfval  39013  hdmap1fval  39050  hdmapfval  39081  hgmapfval  39140  sn-it0e0  39496  pw2f1ocnv  39908  hbtlem7  39999  relexp0a  40347  ntrclscls00  40702  dvconstbi  40972  expgrowth  40973  addrfv  41107  subrfv  41108  mulvfv  41109  refsum2cnlem1  41600  limcperiod  42209  cncfiooiccre  42476  dvbdfbdioolem1  42509  itgioocnicc  42558  fourierdlem73  42760  fourierdlem82  42769  fourierdlem94  42781  fourierdlem103  42790  fourierdlem104  42791  fourierdlem113  42800  sqwvfoura  42809  etransclem46  42861  nnfoctbdjlem  43033  ovn0  43144  smflim  43349  afveu  43648  afv2eu  43733  fvmptrabdm  43788  imasetpreimafvbijlemfo  43861  lighneallem3  44064  mogoldbblem  44177  fpprel2  44198  sbgoldbwt  44234  nnsum4primeseven  44257  nnsum4primesevenALTV  44258  bgoldbtbnd  44266  lmod0rng  44431  rnghmval  44454  lmodvsmdi  44723  lincdifsn  44772  lcoel0  44776  islindeps2  44831  blenn0  44926  nn0sumshdiglemA  44972  itcoval0mpt  45019  rrx2plordisom  45076  aacllem  45268
  Copyright terms: Public domain W3C validator