MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syli 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  4728  elreldm  5035  tz6.12c  5691  rntpos  6429  smores  6551  seqomlem2  6645  f1domg  7064  php  7228  fodomnum  7872  carduniima  7911  cardmin  8373  negn0  10495  sqrmo  11985  grpomndo  21783  elghomlem2  21799  isch3  22593  cgrtriv  25651
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator