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  6016  odi  7010  oeoelem  7029  mapxpen  7469  xadddilem  11249  pcqmul  13912  infpnlem1  13963  neitr  18759  hausflimi  19528  nmoix  20283  nmoleub  20285  metdsre  20404  pthdepisspth  23424  sspph  24206  unoplin  25275  hmoplin  25297  chirredlem1  25745  mdsymlem2  25759  ordtconlem1  26306  heicant  28379  cnambfre  28393  itg2addnclem  28396  ftc1anclem5  28424  rrnequiv  28687  isfldidl  28821  ispridlc  28823  extwwlkfab  30636  reccot  30982  rectan  30983
  Copyright terms: Public domain W3C validator