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

Theorem syld3an1 1274
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 1201 . . 3  |-  ( ( th  /\  ps  /\  ch )  ->  ph )
3 syld3an1.2 . . . 4  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
433com13 1201 . . 3  |-  ( ( th  /\  ps  /\  ph )  ->  ta )
52, 4syld3an3 1273 . 2  |-  ( ( th  /\  ps  /\  ch )  ->  ta )
653com13 1201 1  |-  ( ( ch  /\  ps  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 975
This theorem is referenced by:  npncan  9836  nnpcan  9838  ppncan  9857  div2neg  10263  ltmuldiv  10411  zndvds  18355  subdivcomb1  28580  stoweidlem34  31334  stoweidlem49  31349  stoweidlem57  31357  sigarexp  31543  el0ldepsnzr  32141  atlrelat1  34118  cvlatcvr1  34138  dih11  36062
  Copyright terms: Public domain W3C validator