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  6358  lt2add  9259  nn0seqcvgd  12740  1stcelcls  17187  llyidm  17214  filuni  17580  ballotlemimin  23064  btwnintr  24642  ifscgr  24667  btwnconn1lem12  24721  cvrntr  29614
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