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

Theorem sylanl2 646
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 566 . 2  |-  ( ( ps  /\  ph )  ->  ( ps  /\  ch ) )
3 sylanl2.2 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
42, 3sylan 468 1  |-  ( ( ( ps  /\  ph )  /\  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:  mpanlr1  681  adantlrl  714  adantlrr  715  oesuclem  6961  oelim  6970  mulsub  9783  divsubdiv  10043  vdwlem12  14049  dpjidcl  16547  dpjidclOLD  16554  mplbas2  17527  bwth  18972  cnextfun  19595  elbl4  20110  metucnOLD  20122  metucn  20123  dvradcnv  21845  dchrisum0lem2a  22725  axcontlem4  23148  cnlnadjlem2  25407  chirredlem2  25730  mdsymlem5  25746  sibfof  26656  unichnidl  28756  dmncan2  28802  jm2.26  29276  cvrexchlem  32785
  Copyright terms: Public domain W3C validator