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  6366  oesuclem  6540  oelim  6549  mulsub  9238  divsubdiv  9492  vdwlem12  13055  dpjidcl  15309  dvradcnv  19813  dchrisum0lem2a  20682  cnlnadjlem2  22664  chirredlem2  22987  mdsymlem5  23003  axcontlem4  24667  unichnidl  26759  dmncan2  26805  jm2.26  27198  cvrexchlem  30230
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