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

Theorem sylanl1 648
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 566 . 2  |-  ( (
ph  /\  ch )  ->  ( ps  /\  ch ) )
3 sylanl1.2 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
42, 3sylan 469 1  |-  ( ( ( ph  /\  ch )  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  adantlll  715  adantllr  716  isocnv  6127  odi  7146  oeoelem  7165  mapxpen  7602  xadddilem  11407  pcqmul  14379  infpnlem1  14430  chpdmat  19427  neitr  19767  hausflimi  20566  nmoix  21321  nmoleub  21323  metdsre  21442  pthdepisspth  24697  extwwlkfab  25211  sspph  25887  unoplin  26955  hmoplin  26977  chirredlem1  27425  mdsymlem2  27439  foresf1o  27521  ordtconlem1  28060  heicant  30214  cnambfre  30228  itg2addnclem  30232  ftc1anclem5  30260  ftc1anc  30264  rrnequiv  30497  isfldidl  30631  ispridlc  30633  reccot  33488  rectan  33489
  Copyright terms: Public domain W3C validator