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

Theorem sylanl1 631
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 551 . 2  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )
3 sylanl1.2 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
42, 3sylan 457 1  |-  ( ( ( ph  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  adantlll  698  adantllr  699  isocnv  5843  odi  6593  oeoelem  6612  mapxpen  7043  xadddilem  10630  pcqmul  12922  infpnlem1  12973  hausflimi  17691  nmoix  18254  nmoleub  18256  metdsre  18373  sspph  21449  unoplin  22516  hmoplin  22538  chirredlem1  22986  mdsymlem2  23000  itg2addnclem  25003  rrnequiv  26662  isfldidl  26796  ispridlc  26798  pthdepisspth  28360  reccot  28482  rectan  28483
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 177  df-an 360
  Copyright terms: Public domain W3C validator