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

Theorem sylan2d 468
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 440 . . 3  |-  ( ph  ->  ( ( ch  /\  th )  ->  ta )
)
41, 3syland 467 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ta )
)
54ancomsd 440 1  |-  ( ph  ->  ( ( th  /\  ps )  ->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  syl2and  469  sylan2i  636  swopo  4340  unblem1  7125  unfi  7140  prodgt02  9618  prodge02  9620  lo1mul  12117  infpnlem1  12973  ghmcnp  17813  ulmcaulem  19787  ulmcau  19788  shintcli  21924  ballotlemfc0  23067  ballotlemfcc  23068  wfrlem5  24331  frrlem5  24356  btwnxfr  24751  endofsegid  24780  ltcvrntr  30235  poml4N  30764
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 177  df-an 360
  Copyright terms: Public domain W3C validator