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  4677  elreldm  4982  tz6.12c  5627  rntpos  6331  smores  6453  seqomlem2  6547  f1domg  6966  php  7130  fodomnum  7771  carduniima  7810  cardmin  8273  negn0  10393  sqrmo  11827  grpomndo  21119  elghomlem2  21135  isch3  21929  cgrtriv  25184
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator