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

Theorem syld3an1 1230
Description: A syllogism inference. (Contributed by NM, 7-Jul-2008.)
Hypotheses
Ref Expression
syld3an1.1  |-  ( ( ch  /\  ps  /\  th )  ->  ph )
syld3an1.2  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
Assertion
Ref Expression
syld3an1  |-  ( ( ch  /\  ps  /\  th )  ->  ta )

Proof of Theorem syld3an1
StepHypRef Expression
1 syld3an1.1 . . . 4  |-  ( ( ch  /\  ps  /\  th )  ->  ph )
213com13 1158 . . 3  |-  ( ( th  /\  ps  /\  ch )  ->  ph )
3 syld3an1.2 . . . 4  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
433com13 1158 . . 3  |-  ( ( th  /\  ps  /\  ph )  ->  ta )
52, 4syld3an3 1229 . 2  |-  ( ( th  /\  ps  /\  ch )  ->  ta )
653com13 1158 1  |-  ( ( ch  /\  ps  /\  th )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  npncan  9248  ppncan  9268  div2neg  9662  ltmuldiv  9805  spwpr4  14583  zndvds  16746  subdivcomb1  24967  stoweidlem34  27444  stoweidlem49  27459  stoweidlem57  27467  sigarexp  27510  atlrelat1  29487  cvlatcvr1  29507  dih11  31431
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  df-3an 938
  Copyright terms: Public domain W3C validator