MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syli Structured 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  246  bija  356  equvini  2142  equveli  2143  2eu6  2356  rgen2a  2852  rexraleqim  3197  elreldm  5075  tz6.12c  5897  onminex  6645  rntpos  6991  smores  7076  seqomlem2  7173  f1domg  7593  php  7759  fodomnum  8489  carduniima  8528  cardmin  8990  negn0  10049  sqrmo  13304  grpomndo  26060  elghomlem2OLD  26076  isch3  26880  cgrtriv  30762  wl-lem-moexsb  31811
  Copyright terms: Public domain W3C validator