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

Theorem syli 38
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 32 . 2  |-  ( ph  ->  ( ch  ->  th )
)
41, 3sylcom 30 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  247  bija  357  equvini  2179  equveli  2180  2eu6  2387  rgen2a  2815  rexraleqim  3165  elreldm  5059  tz6.12c  5884  onminex  6634  rntpos  6986  smores  7071  seqomlem2  7168  f1domg  7589  php  7756  fodomnum  8488  carduniima  8527  cardmin  8989  negn0  10048  sqrmo  13315  grpomndo  26074  elghomlem2OLD  26090  isch3  26894  cgrtriv  30769  wl-lem-moexsb  31897
  Copyright terms: Public domain W3C validator