MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylanl2 Structured version   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  6587  oesuclem  6761  oelim  6770  mulsub  9466  divsubdiv  9720  vdwlem12  13350  dpjidcl  15606  cnextfun  18085  elbl4  18596  metucnOLD  18608  metucn  18609  dvradcnv  20327  dchrisum0lem2a  21201  cnlnadjlem2  23561  chirredlem2  23884  mdsymlem5  23900  sibfof  24644  axcontlem4  25871  unichnidl  26595  dmncan2  26641  jm2.26  27027  cvrexchlem  30117
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