MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syld3an1 Structured version   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  9315  ppncan  9335  div2neg  9729  ltmuldiv  9872  spwpr4  14655  zndvds  16822  subdivcomb1  25187  stoweidlem34  27750  stoweidlem49  27765  stoweidlem57  27773  sigarexp  27816  atlrelat1  30056  cvlatcvr1  30076  dih11  32000
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