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

Theorem sylanl1 632
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 552 . 2  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )
3 sylanl1.2 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
42, 3sylan 458 1  |-  ( ( ( ph  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  adantlll  699  adantllr  700  isocnv  5990  odi  6759  oeoelem  6778  mapxpen  7210  xadddilem  10806  pcqmul  13155  infpnlem1  13206  neitr  17167  hausflimi  17934  nmoix  18635  nmoleub  18637  metdsre  18755  pthdepisspth  21429  sspph  22205  unoplin  23272  hmoplin  23294  chirredlem1  23742  mdsymlem2  23756  itg2addnclem  25958  rrnequiv  26236  isfldidl  26370  ispridlc  26372  reccot  27848  rectan  27849
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator