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  2053  equveli  2054  equveliOLD  2055  2eu6  2386  rgen2a  2884  rexraleqim  3222  elreldm  5218  tz6.12c  5876  onminex  6613  rntpos  6958  smores  7013  seqomlem2  7106  f1domg  7525  php  7691  fodomnum  8427  carduniima  8466  cardmin  8928  negn0  11157  sqrmo  13035  grpomndo  25010  elghomlem2  25026  isch3  25821  cgrtriv  29215  wl-lem-moexsb  29580
  Copyright terms: Public domain W3C validator