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

Theorem syland 469
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 427 . . 3  |-  ( ph  ->  ( ch  ->  ( th  ->  ta ) ) )
41, 3syld 43 . 2  |-  ( ph  ->  ( ps  ->  ( th  ->  ta ) ) )
54imp3a 422 1  |-  ( ph  ->  ( ( ps  /\  th )  ->  ta )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  sylan2d  470  syl2and  471  sylani  637  onfununi  6605  lt2add  9515  nn0seqcvgd  13063  1stcelcls  17526  llyidm  17553  filuni  17919  ballotlemimin  24765  btwnintr  25955  ifscgr  25980  btwnconn1lem12  26034  cvrntr  30284
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 179  df-an 362
  Copyright terms: Public domain W3C validator