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  5827  odi  6577  oeoelem  6596  mapxpen  7027  xadddilem  10614  pcqmul  12906  infpnlem1  12957  hausflimi  17675  nmoix  18238  nmoleub  18240  metdsre  18357  sspph  21433  unoplin  22500  hmoplin  22522  chirredlem1  22970  mdsymlem2  22984  rrnequiv  26559  isfldidl  26693  ispridlc  26695  reccot  28228  rectan  28229
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