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  9859  nnpcan  9861  ppncan  9880  div2neg  10288  ltmuldiv  10436  sgrp2nmndlem4  16173  zndvds  18715  subdivcomb1  29323  wsuceq123  29587  mullimc  31825  mullimcf  31832  icccncfext  31893  stoweidlem34  32019  stoweidlem49  32034  stoweidlem57  32042  sigarexp  32279  el0ldepsnzr  33212  atlrelat1  35189  cvlatcvr1  35209  dih11  37135
  Copyright terms: Public domain W3C validator