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  4746  elreldm  5053  tz6.12c  5709  rntpos  6451  smores  6573  seqomlem2  6667  f1domg  7086  php  7250  fodomnum  7894  carduniima  7933  cardmin  8395  negn0  10518  sqrmo  12012  grpomndo  21887  elghomlem2  21903  isch3  22697  cgrtriv  25840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator