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  6211  odi  7230  oeoelem  7249  mapxpen  7685  xadddilem  11495  pcqmul  14254  infpnlem1  14305  chpdmat  19215  neitr  19554  hausflimi  20354  nmoix  21109  nmoleub  21111  metdsre  21230  pthdepisspth  24448  extwwlkfab  24962  sspph  25642  unoplin  26711  hmoplin  26733  chirredlem1  27181  mdsymlem2  27195  foresf1o  27275  ordtconlem1  27779  heicant  30024  cnambfre  30038  itg2addnclem  30041  ftc1anclem5  30069  ftc1anc  30073  rrnequiv  30306  isfldidl  30440  ispridlc  30442  reccot  32887  rectan  32888
  Copyright terms: Public domain W3C validator