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

Theorem sylan2d 479
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 451 . . 3  |-  ( ph  ->  ( ( ch  /\  th )  ->  ta )
)
41, 3syland 478 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ta )
)
54ancomsd 451 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ta )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  syl2and  480  sylan2i  648  swopo  4638  unblem1  7552  unfi  7567  prodgt02  10163  prodge02  10165  lo1mul  13089  infpnlem1  13954  ghmcnp  19527  ulmcaulem  21744  ulmcau  21745  shintcli  24555  ballotlemfc0  26723  ballotlemfcc  26724  wfrlem5  27575  frrlem5  27619  btwnxfr  27934  endofsegid  27963  bj-bary1lem1  32175  ltcvrntr  32641  poml4N  33170
  Copyright terms: Public domain W3C validator