MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylanl1 Structured version   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  6042  odi  6814  oeoelem  6833  mapxpen  7265  xadddilem  10865  pcqmul  13219  infpnlem1  13270  neitr  17236  hausflimi  18004  nmoix  18755  nmoleub  18757  metdsre  18875  pthdepisspth  21566  sspph  22348  unoplin  23415  hmoplin  23437  chirredlem1  23885  mdsymlem2  23899  cnambfre  26245  itg2addnclem  26246  ftc1anclem5  26274  rrnequiv  26535  isfldidl  26669  ispridlc  26671  reccot  28438  rectan  28439
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