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

Theorem sylanl2 633
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 553 . 2  |-  ( ( ps  /\  ph )  ->  ( ps  /\  ch ) )
3 sylanl2.2 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
42, 3sylan 458 1  |-  ( ( ( ps  /\  ph )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpanlr1  668  adantlrl  701  adantlrr  702  riotasv2dOLD  6531  oesuclem  6705  oelim  6714  mulsub  9408  divsubdiv  9662  vdwlem12  13287  dpjidcl  15543  cnextfun  18016  elbl4  18483  metucn  18490  dvradcnv  20204  dchrisum0lem2a  21078  cnlnadjlem2  23419  chirredlem2  23742  mdsymlem5  23758  axcontlem4  25620  unichnidl  26332  dmncan2  26378  jm2.26  26764  cvrexchlem  29533
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator