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

Theorem sylan9eq 2876
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 2841 . 2 ((𝐴 = 𝐵𝐵 = 𝐶) → 𝐴 = 𝐶)
41, 2, 3syl2an 595 1 ((𝜑𝜓) → 𝐴 = 𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2814
This theorem is referenced by:  sylan9req  2877  sylan9eqr  2878  difeq12  4093  uneq12  4133  ineq12  4183  ssdifim  4238  ifeq12  4482  ifbi  4486  ifeq12da  4497  preq12  4665  prprc  4697  opeq12  4799  opthwiener  5396  opthhausdorff0  5400  xpeq12  5574  sosn  5632  nfimad  5932  coi2  6110  funprg  6402  funtpg  6403  funcnvtp  6411  funcnvqp  6412  funimass1  6430  fimadmfoALT  6595  f1orescnv  6624  resdif  6629  fvmpt2  6772  fvmptnf  6783  fveqressseq  6840  oveq12  7154  cbvmpov  7238  ovmpog  7298  caofinvl  7425  eqopi  7716  el2mpocsbcl  7771  fmpoco  7781  mposn  7789  supp0cosupp0  7863  supp0cosupp0OLD  7864  imacosupp  7865  mpocurryd  7926  fvmpocurryd  7928  wrecseq123  7939  rdgsucmptf  8055  frsucmpt  8064  oevn0  8131  oa0r  8154  om1r  8159  oe1m  8161  omass  8196  oeoalem  8212  oeoa  8213  oeoe  8215  qseq12  8337  map0g  8438  xpcomco  8596  sbthlem4  8619  sbthlem5  8620  xpmapenlem  8673  phplem3  8687  phplem4  8688  unxpdomlem3  8713  funsnfsupp  8846  ordtypelem7  8977  cardennn  9401  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  12368  rpnnen1lem5  12370  xaddpnf1  12609  xaddpnf2  12610  xaddmnf1  12611  xaddmnf2  12612  rexadd  12615  xnn0xaddcl  12618  xaddnemnf  12619  xaddnepnf  12620  xadddilem  12677  addmodlteq  13304  om2uzrani  13310  om2uzrdg  13314  seqf1olem2  13400  seqf1o  13401  modexp  13589  faclbnd4lem3  13645  hashunsng  13743  hashwrdn  13888  lsw1  13909  swrdfv  14000  swrdccat  14087  ccats1pfxeqbi  14094  revfv  14115  cshwsublen  14148  wrdlen2  14296  wrdl2exs2  14298  wwlktovf1  14311  relexp0  14372  relexpcnv  14384  shftcan1  14432  remul2  14479  immul2  14486  sumss  15071  geomulcvg  15222  fprodss  15292  binomfallfaclem2  15384  bpolylem  15392  ef0lem  15422  efieq1re  15542  rpnnen2lem1  15557  ruclem3  15576  dvdsnegb  15617  dvdscmul  15626  dvds2ln  15632  dvds2add  15633  dvds2sub  15634  gcdn0val  15837  rpmulgcd  15896  lcmn0val  15929  odzval  16118  pcval  16171  pcmpt  16218  prmreclem4  16245  1arithlem2  16250  vdwlem8  16314  ramcl2lem  16335  ramtcl  16336  ramtub  16338  ramcl2  16342  ramcl  16355  setsval  16503  prfcl  17443  curf1cl  17468  curfcl  17472  hofcl  17499  yonedalem4c  17517  psssdm  17816  grplactval  18141  mulgnn0gsum  18174  cntzval  18391  f1omvdco2  18507  pmtrfinv  18520  psgnunilem5  18553  odlem2  18598  gexlem2  18638  lsmvalx  18695  efgtval  18780  efgredlema  18797  vrgpval  18824  cyggex  18949  gsumcom2  19026  fincygsubgodd  19165  dvdsrtr  19333  abvtrivd  19542  lmhmco  19746  reslmhm  19755  lvecinv  19816  mplmon2  20203  subrgasclcl  20209  coe1fv  20304  coe1fzgsumdlem  20399  evl1gsumdlem  20449  zrhmulg  20587  znzrhval  20623  ocvval  20741  mat1dimscm  21014  dmatid  21034  scmatdmat  21054  mavmul0g  21092  1marepvmarrepid  21114  mdetunilem2  21152  gsummatr01lem3  21196  gsummatr01  21198  smadiadetlem3  21207  m2cpminvid2lem  21292  chpdmatlem2  21377  isopn3  21604  cnpval  21774  ptbasfi  22119  dfac14  22156  cnmptkk  22221  xkofvcn  22222  cnmptk1p  22223  cnmptk2  22224  xkocnv  22352  flfval  22528  ptcmplem3  22592  ptcmpg  22595  tmdmulg  22630  prdsxmslem2  23068  subgnm2  23172  nmoval  23253  fsum2cn  23408  pcovalg  23545  isclmp  23630  cphnm  23726  tcphnmval  23761  ovolctb  24020  ioorcl  24107  uniioombllem2  24113  itg1addlem3  24228  itg1climres  24244  itg2uba  24273  itg2splitlem  24278  elcpn  24460  dvexp  24479  dvexp2  24480  rolle  24516  cmvth  24517  mvth  24518  dvlip  24519  dvlipcn  24520  dvlip2  24521  dveq0  24526  dv11cn  24527  lhop1lem  24539  lhop2  24541  lhop  24542  dvcvx  24546  ftc2ditglem  24571  itgsubstlem  24574  ig1pval  24695  elply2  24715  coeid2  24758  coemul  24771  taylthlem2  24891  ulmdvlem1  24917  mtest  24921  pserval2  24928  abelthlem1  24948  abelthlem3  24950  abelthlem8  24956  abelthlem9  24957  pige3ALT  25034  0cxp  25176  leibpi  25448  igamgam  25554  mule1  25653  bposlem5  25792  lgsval3  25819  lgsdinn0  25849  dchrvmasumlem1  25999  dchrisum0flblem1  26012  rpvmasum2  26016  padicval  26121  axsegconlem1  26631  ax5seglem9  26651  axpasch  26655  axeuclidlem  26676  axcontlem2  26679  finsumvtxdg2ssteplem4  27258  usgr2wlkspthlem2  27467  crctcshlem4  27526  wwlknp  27549  wlkiswwlks2lem3  27577  wwlksnred  27598  wwlksnextproplem2  27617  umgrwwlks2on  27664  clwlkclwwlklem2a  27704  clwwisshclwwsn  27722  clwwlknlbonbgr1  27745  clwwlkn1loopb  27749  clwwlkf  27754  clwwlkext2edg  27763  wwlksext2clwwlk  27764  erclwwlknsym  27777  erclwwlkntr  27778  clwwlknon1  27804  clwwlknonex2  27816  eupth2lem3lem3  27937  eucrct2eupth  27952  fusgreghash2wspv  28042  2clwwlk2clwwlklem  28053  2clwwlk2clwwlk  28057  numclwwlk1lem2f1  28064  grpoidinvlem4  28212  grpoinvval  28228  grpodivval  28240  ipval  28408  sspgval  28434  sspsval  28436  sspnval  28442  nmooval  28468  ipasslem1  28536  ipasslem4  28539  hial0  28807  hial02  28808  ocsh  28988  pjhval  29102  hosval  29445  homval  29446  hodval  29447  hfsval  29448  hfmval  29449  braval  29649  kbval  29659  eigvalval  29665  0hmop  29688  adj0  29699  lnopeq0i  29712  nmopcoi  29800  pjclem4  29904  pj3si  29912  hstoh  29937  strlem3a  29957  hstrlem3a  29965  mdexchi  30040  atcv0eq  30084  atcv1  30085  fpwrelmap  30396  cycpmco2lem4  30699  cycpmco2lem5  30700  smatfval  30960  measxun2  31369  measdivcst  31383  measdivcstALTV  31384  ddeval1  31393  ddeval0  31394  ballotlemfp1  31649  signswmnd  31727  signstfvneq0  31742  signstfvc  31744  ftc2re  31769  itgexpif  31777  bnj1128  32160  subfacp1lem3  32327  subfacp1lem5  32329  cvmlift2lem3  32450  msubco  32676  altopthsn  33320  fnetr  33597  fnejoin2  33615  bj-evalid  34262  finxpreclem3  34557  finxpreclem5  34559  finxpreclem6  34560  curf  34752  curunc  34756  matunitlindf  34772  poimirlem4  34778  poimirlem25  34799  mblfinlem2  34812  mblfinlem3  34813  mbfresfi  34820  itg2addnclem  34825  itg2addnc  34828  ftc1anclem5  34853  isbnd3  34945  bndss  34947  grposnOLD  35043  ghomco  35052  xrneq12  35517  lkrval  36106  pmapval  36775  polvalN  36923  watvalN  37011  ldilset  37127  ltrnset  37136  dilsetN  37171  trnsetN  37174  trlset  37179  trlval  37180  cdleme16b  37297  cdleme31fv1  37409  cdlemg1idlemN  37590  tgrpset  37763  tendoset  37777  erngset  37818  erngplus  37821  erngmul  37824  erngset-rN  37826  erngplus-rN  37829  dvaset  38023  dvaplusg  38027  dvamulr  38030  dvavadd  38033  dvavsca  38035  diafval  38049  dvhset  38099  dvhmulr  38104  dvhvadd  38110  dvhvsca  38119  docafvalN  38140  djafvalN  38152  dibfval  38159  dicfval  38193  dihfval  38249  dihval  38250  dihvalc  38251  dihvalb  38255  dochfval  38368  djhfval  38415  lcdval  38607  mapdfval  38645  mapdn0  38687  hvmapfval  38777  hdmap1fval  38814  hdmapfval  38845  hgmapfval  38904  pw2f1ocnv  39514  hbtlem7  39605  relexp0a  39941  ntrclscls00  40296  dvconstbi  40546  expgrowth  40547  addrfv  40681  subrfv  40682  mulvfv  40683  refsum2cnlem1  41174  limcperiod  41789  cncfiooiccre  42058  dvbdfbdioolem1  42093  itgioocnicc  42142  fourierdlem73  42345  fourierdlem82  42354  fourierdlem94  42366  fourierdlem103  42375  fourierdlem104  42376  fourierdlem113  42385  sqwvfoura  42394  etransclem46  42446  nnfoctbdjlem  42618  ovn0  42729  smflim  42934  afveu  43233  afv2eu  43318  fvmptrabdm  43373  lighneallem3  43619  mogoldbblem  43732  fpprel2  43753  sbgoldbwt  43789  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  bgoldbtbnd  43821  lmod0rng  44037  rnghmval  44060  lmodvsmdi  44328  lincdifsn  44377  lcoel0  44381  islindeps2  44436  blenn0  44531  nn0sumshdiglemA  44577  rrx2plordisom  44608  aacllem  44800
  Copyright terms: Public domain W3C validator