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

Theorem syli 33
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 27 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3sylcom 25 1  |-  ( ps 
->  ( ph  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ibd  234  bija  344  onminex  4598  elreldm  4903  tz6.12c  5547  rntpos  6247  smores  6369  seqomlem2  6463  f1domg  6881  php  7045  fodomnum  7684  carduniima  7723  cardmin  8186  negn0  10304  sqrmo  11737  grpomndo  21013  elghomlem2  21029  isch3  21821  cgrtriv  24625  prj1b  25079  prj3  25080  oriso  25214  inttop4  25517
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator