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  7172  oelim  7181  mulsub  9995  divsubdiv  10256  vdwlem12  14365  dpjidcl  16897  dpjidclOLD  16904  mplbas2  17905  monmat2matmon  19092  bwth  19676  cnextfun  20299  elbl4  20814  metucnOLD  20826  metucn  20827  dvradcnv  22550  dchrisum0lem2a  23430  axcontlem4  23946  cnlnadjlem2  26663  chirredlem2  26986  mdsymlem5  27002  sibfof  27922  unichnidl  30031  dmncan2  30077  jm2.26  30548  lcmneg  30809  fourierdlem74  31481  fourierdlem75  31482  fourierdlem83  31490  cvrexchlem  34215
  Copyright terms: Public domain W3C validator