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

Theorem syli 33
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 27 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3sylcom 25 1  |-  ( ps 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ibd  234  bija  344  onminex  4614  elreldm  4919  tz6.12c  5563  rntpos  6263  smores  6385  seqomlem2  6479  f1domg  6897  php  7061  fodomnum  7700  carduniima  7739  cardmin  8202  negn0  10320  sqrmo  11753  grpomndo  21029  elghomlem2  21045  isch3  21837  cgrtriv  24697  prj1b  25182  prj3  25183  oriso  25317  inttop4  25620
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator