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  sbequi  2110  onminex  4787  elreldm  5094  tz6.12c  5750  rntpos  6492  smores  6614  seqomlem2  6708  f1domg  7127  php  7291  fodomnum  7938  carduniima  7977  cardmin  8439  negn0  10562  sqrmo  12057  grpomndo  21934  elghomlem2  21950  isch3  22744  cgrtriv  25936
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator