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

Theorem syli 35
Description: Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.)
Hypotheses
Ref Expression
syli.1  |-  ( ps 
->  ( ph  ->  ch ) )
syli.2  |-  ( ch 
->  ( ph  ->  th )
)
Assertion
Ref Expression
syli  |-  ( ps 
->  ( ph  ->  th )
)

Proof of Theorem syli
StepHypRef Expression
1 syli.1 . 2  |-  ( ps 
->  ( ph  ->  ch ) )
2 syli.2 . . 3  |-  ( ch 
->  ( ph  ->  th )
)
32com12 29 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3sylcom 27 1  |-  ( ps 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ibd  235  bija  345  onminex  4779  elreldm  5086  tz6.12c  5742  rntpos  6484  smores  6606  seqomlem2  6700  f1domg  7119  php  7283  fodomnum  7930  carduniima  7969  cardmin  8431  negn0  10554  sqrmo  12049  grpomndo  21926  elghomlem2  21942  isch3  22736  cgrtriv  25928
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator