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

Theorem sylan2d 480
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 452 . . 3  |-  ( ph  ->  ( ( ch  /\  th )  ->  ta )
)
41, 3syland 479 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ta )
)
54ancomsd 452 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ta )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  syl2and  481  sylan2i  653  swopo  4754  wfrlem5  7025  unblem1  7806  unfi  7821  prodgt02  10429  prodge02  10431  lo1mul  13599  infpnlem1  14637  ghmcnp  20905  ulmcaulem  23081  ulmcau  23082  shintcli  26661  ballotlemfc0  28937  ballotlemfcc  28938  frrlem5  30091  btwnxfr  30394  endofsegid  30423  bj-bary1lem1  31241  ltcvrntr  32441  poml4N  32970
  Copyright terms: Public domain W3C validator