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

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

Proof of Theorem syland
StepHypRef Expression
1 syland.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
2 syland.2 . . . 4  |-  ( ph  ->  ( ( ch  /\  th )  ->  ta )
)
32expd 437 . . 3  |-  ( ph  ->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syld 45 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ta ) ) )
54impd 432 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  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:  sylan2d  484  syl2and  485  sylani  658  onfununi  7068  lt2add  10098  nn0seqcvgd  14500  1stcelcls  20407  llyidm  20434  filuni  20831  ballotlemimin  29164  btwnintr  30571  ifscgr  30596  btwnconn1lem12  30650  poimir  31677  cvrntr  32699
  Copyright terms: Public domain W3C validator