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

Theorem sylanl2 651
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 569 . 2  |-  ( ( ps  /\  ph )  ->  ( ps  /\  ch ) )
3 sylanl2.2 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
42, 3sylan 471 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  686  adantlrl  719  adantlrr  720  oesuclem  6980  oelim  6989  mulsub  9802  divsubdiv  10062  vdwlem12  14068  dpjidcl  16572  dpjidclOLD  16579  mplbas2  17566  bwth  19028  cnextfun  19651  elbl4  20166  metucnOLD  20178  metucn  20179  dvradcnv  21901  dchrisum0lem2a  22781  axcontlem4  23228  cnlnadjlem2  25487  chirredlem2  25810  mdsymlem5  25826  sibfof  26741  unichnidl  28850  dmncan2  28896  jm2.26  29370  cvrexchlem  33082
  Copyright terms: Public domain W3C validator