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

Theorem sylanl2 649
Description: A syllogism inference. (Contributed by NM, 1-Jan-2005.)
Hypotheses
Ref Expression
sylanl2.1  |-  ( ph  ->  ch )
sylanl2.2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
Assertion
Ref Expression
sylanl2  |-  ( ( ( ps  /\  ph )  /\  th )  ->  ta )

Proof of Theorem sylanl2
StepHypRef Expression
1 sylanl2.1 . . 3  |-  ( ph  ->  ch )
21anim2i 567 . 2  |-  ( ( ps  /\  ph )  ->  ( ps  /\  ch ) )
3 sylanl2.2 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
42, 3sylan 469 1  |-  ( ( ( ps  /\  ph )  /\  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:  mpanlr1  684  adantlrl  717  adantlrr  718  oesuclem  7115  oelim  7124  mulsub  9939  divsubdiv  10199  vdwlem12  14535  dpjidcl  17243  dpjidclOLD  17250  mplbas2  18270  monmat2matmon  19433  bwth  20019  cnextfun  20672  elbl4  21187  metucnOLD  21199  metucn  21200  dvradcnv  22924  dchrisum0lem2a  23842  axcontlem4  24416  cnlnadjlem2  27128  chirredlem2  27451  mdsymlem5  27467  sibfof  28505  unichnidl  30634  dmncan2  30680  jm2.26  31150  radcnvrat  31403  lcmneg  31417  binomcxplemnotnn0  31469  dvnmptdivc  31940  fourierdlem64  32158  fourierdlem74  32168  fourierdlem75  32169  fourierdlem83  32177  etransclem35  32257  cvrexchlem  35595
  Copyright terms: Public domain W3C validator