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

Theorem syld3an1 1264
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 1192 . . 3  |-  ( ( th  /\  ps  /\  ch )  ->  ph )
3 syld3an1.2 . . . 4  |-  ( (
ph  /\  ps  /\  th )  ->  ta )
433com13 1192 . . 3  |-  ( ( th  /\  ps  /\  ph )  ->  ta )
52, 4syld3an3 1263 . 2  |-  ( ( th  /\  ps  /\  ch )  ->  ta )
653com13 1192 1  |-  ( ( ch  /\  ps  /\  th )  ->  ta )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 967
This theorem is referenced by:  npncan  9630  nnpcan  9632  ppncan  9651  div2neg  10054  ltmuldiv  10202  zndvds  17982  subdivcomb1  27384  stoweidlem34  29829  stoweidlem49  29844  stoweidlem57  29852  sigarexp  29895  el0ldepsnzr  31001  atlrelat1  32966  cvlatcvr1  32986  dih11  34910
  Copyright terms: Public domain W3C validator