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

Theorem sylan2d 484
Description: A syllogism deduction. (Contributed by NM, 15-Dec-2004.)
Hypotheses
Ref Expression
sylan2d.1  |-  ( ph  ->  ( ps  ->  ch ) )
sylan2d.2  |-  ( ph  ->  ( ( th  /\  ch )  ->  ta )
)
Assertion
Ref Expression
sylan2d  |-  ( ph  ->  ( ( th  /\  ps )  ->  ta )
)

Proof of Theorem sylan2d
StepHypRef Expression
1 sylan2d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylan2d.2 . . . 4  |-  ( ph  ->  ( ( th  /\  ch )  ->  ta )
)
32ancomsd 455 . . 3  |-  ( ph  ->  ( ( ch  /\  th )  ->  ta )
)
41, 3syland 483 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ta )
)
54ancomsd 455 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ta )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  syl2and  485  sylan2i  659  swopo  4781  wfrlem5  7045  unblem1  7826  unfi  7841  prodgt02  10452  prodge02  10454  lo1mul  13679  infpnlem1  14842  ghmcnp  21116  ulmcaulem  23336  ulmcau  23337  shintcli  26968  ballotlemfc0  29321  ballotlemfcc  29322  frrlem5  30513  btwnxfr  30816  endofsegid  30845  bj-bary1lem1  31668  ltcvrntr  32908  poml4N  33437
  Copyright terms: Public domain W3C validator