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

Theorem sylan9eq 2348
Description: An equality transitivity deduction. (Contributed by NM, 8-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
sylan9eq.1  |-  ( ph  ->  A  =  B )
sylan9eq.2  |-  ( ps 
->  B  =  C
)
Assertion
Ref Expression
sylan9eq  |-  ( (
ph  /\  ps )  ->  A  =  C )

Proof of Theorem sylan9eq
StepHypRef Expression
1 sylan9eq.1 . 2  |-  ( ph  ->  A  =  B )
2 sylan9eq.2 . 2  |-  ( ps 
->  B  =  C
)
3 eqtr 2313 . 2  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
41, 2, 3syl2an 463 1  |-  ( (
ph  /\  ps )  ->  A  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    = wceq 1632
This theorem is referenced by:  sylan9req  2349  sylan9eqr  2350  difeq12  3302  uneq12  3337  ineq12  3378  ifeq12  3591  ifbi  3595  preq12  3721  prprc  3751  preq12b  3804  opeq12  3814  opthwiener  4284  ordintdif  4457  xpeq12  4724  sosn  4775  nfimad  5037  coi2  5205  funimass1  5341  f1orescnv  5504  resdif  5510  fvmpt2  5624  fvmptnf  5633  oveq12  5883  cbvmpt2v  5942  ovmpt2g  5998  caofinvl  6120  eqopi  6172  fmpt2co  6218  rdgsucmptf  6457  frsucmpt  6466  abianfplem  6486  oevn0  6530  oa0r  6553  om1r  6557  oe1m  6559  omass  6594  oeoalem  6610  oeoa  6611  oeoe  6613  map0g  6823  xpcomco  6968  sbthlem4  6990  sbthlem5  6991  xpmapenlem  7044  phplem3  7058  phplem4  7059  unxpdomlem3  7085  ordtypelem7  7255  cardennn  7632  dfac9  7778  cdaassen  7824  alephsing  7918  axcc3  8080  ac6num  8122  konigthlem  8206  canthp1lem2  8291  ordpipq  8582  ltrnq  8619  addclprlem2  8657  mulclprlem  8659  prlem934  8673  prlem936  8687  mulcmpblnrlem  8711  addcnsr  8773  mulcnsr  8774  axcnre  8802  recex  9416  uzindOLD  10122  rpnnen1lem3  10360  rpnnen1lem5  10362  xaddpnf1  10569  xaddpnf2  10570  xaddmnf1  10571  xaddmnf2  10572  rexadd  10575  xaddnemnf  10577  xaddnepnf  10578  xadddilem  10630  om2uzrani  11031  om2uzrdg  11035  seqf1olem2  11102  seqf1o  11103  modexp  11252  faclbnd4lem3  11324  hashunsng  11383  swrdfv  11473  revfv  11497  shftcan1  11594  remul2  11631  immul2  11638  sumss  12213  geomulcvg  12348  ef0lem  12376  efieq1re  12495  rpnnen2lem1  12509  ruclem3  12527  dvdsnegb  12562  dvdscmul  12571  dvds2ln  12575  dvds2add  12576  dvds2sub  12577  gcdn0val  12705  rpmulgcd  12750  odzval  12872  pcval  12913  pcmpt  12956  prmreclem4  12982  1arithlem2  12987  vdwlem8  13051  ramcl2lem  13072  ramtcl  13073  ramtub  13075  ramcl2  13079  ramcl  13092  setsval  13188  prfcl  13993  curf1cl  14018  curfcl  14022  hofcl  14049  yonedalem4c  14067  lubval  14129  glbval  14134  joinval  14138  meetval  14145  psssdm  14341  grplactval  14579  cntzval  14813  odlem2  14870  gexlem2  14909  lsmvalx  14966  efgtval  15048  efgredlema  15065  vrgpval  15092  cyggex  15200  gsumcom2  15242  dvdsrtr  15450  abvtrivd  15621  lmhmco  15816  reslmhm  15825  lvecinv  15882  mplmon2  16250  subrgasclcl  16256  coe1fv  16303  zrhmulg  16480  znzrhval  16516  ocvval  16583  isopn3  16819  cnpval  16982  ptbasfi  17292  dfac14  17328  cnmptkk  17393  xkofvcn  17394  cnmptk1p  17395  cnmptk2  17396  xkocnv  17521  flfval  17701  ptcmplem3  17764  ptcmpg  17767  tmdmulg  17791  prdsxmslem2  18091  subgnm2  18166  nmoval  18240  fsum2cn  18391  pcovalg  18526  cphnm  18645  tchnmval  18676  ovolctb  18865  ioorcl  18948  uniioombllem2  18954  itg1addlem3  19069  itg1climres  19085  itg2uba  19114  itg2splitlem  19119  elcpn  19299  dvexp  19318  dvexp2  19319  rolle  19353  cmvth  19354  mvth  19355  dvlip  19356  dvlipcn  19357  dvlip2  19358  dveq0  19363  dv11cn  19364  lhop1lem  19376  lhop2  19378  lhop  19379  dvcvx  19383  ftc2ditglem  19408  itgsubstlem  19411  ig1pval  19574  elply2  19594  coeid2  19637  coemul  19649  taylthlem2  19769  ulmdvlem1  19793  mtest  19797  pserval2  19803  abelthlem1  19823  abelthlem3  19825  abelthlem8  19831  abelthlem9  19832  pige3  19901  0cxp  20029  leibpi  20254  mule1  20402  bposlem5  20543  lgsval3  20569  lgsdinn0  20595  dchrvmasumlem1  20660  dchrisum0flblem1  20673  rpvmasum2  20677  padicval  20782  grpoidinvlem4  20890  grposn  20898  grpoinvval  20908  grpodivval  20926  gxval  20941  gxnn0add  20957  subgoov  20988  ablosn  21030  ipval  21292  sspgval  21321  sspsval  21323  sspnval  21329  nmooval  21357  ipasslem1  21425  ipasslem4  21428  hial0  21697  hial02  21698  ocsh  21878  pjhval  21992  hosval  22336  homval  22337  hodval  22338  hfsval  22339  hfmval  22340  braval  22540  kbval  22550  eigvalval  22556  0hmop  22579  adj0  22590  lnopeq0i  22603  nmopcoi  22691  pjclem4  22795  pj3si  22803  hstoh  22828  strlem3a  22848  hstrlem3a  22856  mdexchi  22931  atcv0eq  22975  atcv1  22976  fvmpt2f  23239  measxun2  23553  measdivcstOLD  23566  measdivcst  23567  subfacp1lem3  23728  subfacp1lem5  23730  cvmlift2lem3  23851  vdgrval  23905  relexp1  24042  relexpcnv  24044  relexpadd  24050  altopthsn  24567  axsegconlem1  24617  ax5seglem9  24637  axpasch  24641  axeuclidlem  24662  axcontlem2  24665  bpolylem  24855  valpr  25261  1ded  25841  isfuna  25937  fnetr  26389  reftr  26392  fnejoin2  26421  isbnd3  26611  bndss  26613  ghomco  26676  pw2f1ocnv  27233  hbtlem7  27432  f1omvdco2  27494  pmtrfinv  27505  dvconstbi  27654  expgrowth  27655  addrfv  27777  subrfv  27778  mulvfv  27779  afveu  28121  nbgraop  28274  constr3pthlem3  28403  bnj1128  29336  lkrval  29900  pmapval  30568  polvalN  30716  watvalN  30804  ldilset  30920  ltrnset  30929  dilsetN  30964  trnsetN  30967  trlset  30972  trlval  30973  cdleme16b  31090  cdleme31fv1  31202  cdlemg1idlemN  31383  tgrpset  31556  tendoset  31570  erngset  31611  erngplus  31614  erngmul  31617  erngset-rN  31619  erngplus-rN  31622  dvaset  31816  dvaplusg  31820  dvamulr  31823  dvavadd  31826  dvavsca  31828  diafval  31843  dvhset  31893  dvhmulr  31898  dvhvadd  31904  dvhvsca  31913  docafvalN  31934  djafvalN  31946  dibfval  31953  dicfval  31987  dihfval  32043  dihval  32044  dihvalc  32045  dihvalb  32049  dochfval  32162  djhfval  32209  lcdval  32401  mapdfval  32439  mapdn0  32481  hvmapfval  32571  hdmap1fval  32609  hdmapfval  32642  hgmapfval  32701
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289
  Copyright terms: Public domain W3C validator