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

Theorem sylan2d 482
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 454 . . 3  |-  ( ph  ->  ( ( ch  /\  th )  ->  ta )
)
41, 3syland 481 . 2  |-  ( ph  ->  ( ( ps  /\  th )  ->  ta )
)
54ancomsd 454 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  483  sylan2i  655  swopo  4803  unblem1  7761  unfi  7776  prodgt02  10377  prodge02  10379  lo1mul  13399  infpnlem1  14276  ghmcnp  20341  ulmcaulem  22516  ulmcau  22517  shintcli  25909  ballotlemfc0  28057  ballotlemfcc  28058  wfrlem5  28910  frrlem5  28954  btwnxfr  29269  endofsegid  29298  bj-bary1lem1  33627  ltcvrntr  34095  poml4N  34624
  Copyright terms: Public domain W3C validator