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

Theorem syland 467
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 )
)
32exp3a 425 . . 3  |-  ( ph  ->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syld 40 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ta ) ) )
54imp3a 420 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  sylan2d  468  syl2and  469  sylani  635  onfununi  6374  lt2add  9275  nn0seqcvgd  12756  1stcelcls  17203  llyidm  17230  filuni  17596  ballotlemimin  23080  btwnintr  24714  ifscgr  24739  btwnconn1lem12  24793  cvrntr  30236
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