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

Theorem sylanl2 632
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 552 . 2  |-  ( ( ps  /\  ph )  ->  ( ps  /\  ch ) )
3 sylanl2.2 . 2  |-  ( ( ( ps  /\  ch )  /\  th )  ->  ta )
42, 3sylan 457 1  |-  ( ( ( ps  /\  ph )  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpanlr1  667  adantlrl  700  adantlrr  701  riotasv2dOLD  6350  oesuclem  6524  oelim  6533  mulsub  9222  divsubdiv  9476  vdwlem12  13039  dpjidcl  15293  dvradcnv  19797  dchrisum0lem2a  20666  cnlnadjlem2  22648  chirredlem2  22971  mdsymlem5  22987  axcontlem4  24595  unichnidl  26656  dmncan2  26702  jm2.26  27095  cvrexchlem  29608
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 177  df-an 360
  Copyright terms: Public domain W3C validator