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

Theorem syli 37
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 31 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3sylcom 29 1  |-  ( ps 
->  ( ph  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  ibd  243  bija  355  equvini  2073  equveli  2074  equveliOLD  2075  2eu6  2369  rgen2a  2870  rexraleqim  3211  elreldm  5217  tz6.12c  5875  onminex  6627  rntpos  6970  smores  7025  seqomlem2  7118  f1domg  7537  php  7703  fodomnum  8441  carduniima  8480  cardmin  8942  negn0  11178  sqrmo  13066  grpomndo  25324  elghomlem2OLD  25340  isch3  26135  cgrtriv  29627  wl-lem-moexsb  29992
  Copyright terms: Public domain W3C validator