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

Theorem syld3an1 1259
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 1187 . . 3  |-  ( ( th  /\  ps  /\  ch )  ->  ph )
3 syld3an1.2 . . . 4  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
433com13 1187 . . 3  |-  ( ( th  /\  ps  /\  ph )  ->  ta )
52, 4syld3an3 1258 . 2  |-  ( ( th  /\  ps  /\  ch )  ->  ta )
653com13 1187 1  |-  ( ( ch  /\  ps  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 960
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 962
This theorem is referenced by:  npncan  9620  nnpcan  9622  ppncan  9641  div2neg  10044  ltmuldiv  10192  zndvds  17826  subdivcomb1  27233  stoweidlem34  29677  stoweidlem49  29692  stoweidlem57  29700  sigarexp  29743  el0ldepsnzr  30750  atlrelat1  32579  cvlatcvr1  32599  dih11  34523
  Copyright terms: Public domain W3C validator