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

Theorem sylanl1 650
Description: A syllogism inference. (Contributed by NM, 10-Mar-2005.)
Hypotheses
Ref Expression
sylanl1.1  |-  ( ph  ->  ps )
sylanl1.2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
Assertion
Ref Expression
sylanl1  |-  ( ( ( ph  /\  ch )  /\  th )  ->  ta )

Proof of Theorem sylanl1
StepHypRef Expression
1 sylanl1.1 . . 3  |-  ( ph  ->  ps )
21anim1i 568 . 2  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )
3 sylanl1.2 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
42, 3sylan 471 1  |-  ( ( ( ph  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  adantlll  717  adantllr  718  isocnv  6205  odi  7218  oeoelem  7237  mapxpen  7673  xadddilem  11475  pcqmul  14225  infpnlem1  14276  chpdmat  19102  neitr  19440  hausflimi  20209  nmoix  20964  nmoleub  20966  metdsre  21085  pthdepisspth  24238  extwwlkfab  24753  sspph  25432  unoplin  26501  hmoplin  26523  chirredlem1  26971  mdsymlem2  26985  ordtconlem1  27528  heicant  29613  cnambfre  29627  itg2addnclem  29630  ftc1anclem5  29658  rrnequiv  29921  isfldidl  30055  ispridlc  30057  adantlllr  30949  reccot  32108  rectan  32109
  Copyright terms: Public domain W3C validator