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

Theorem sylcom 30
Description: Syllogism inference with commutation of antecedents. (Contributed by NM, 29-Aug-2004.) (Proof shortened by Mel L. O'Cat, 2-Feb-2006.) (Proof shortened by Stefan Allan, 23-Feb-2006.)
Hypotheses
Ref Expression
sylcom.1  |-  ( ph  ->  ( ps  ->  ch ) )
sylcom.2  |-  ( ps 
->  ( ch  ->  th )
)
Assertion
Ref Expression
sylcom  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem sylcom
StepHypRef Expression
1 sylcom.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 sylcom.2 . . 3  |-  ( ps 
->  ( ch  ->  th )
)
32a2i 14 . 2  |-  ( ( ps  ->  ch )  ->  ( ps  ->  th )
)
41, 3syl 17 1  |-  ( ph  ->  ( ps  ->  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:  syl5com  31  syl6  34  syli  38  mpbidi  219  2eu6  2359  dmcosseq  5053  iss  5109  funopg  5571  limuni3  6632  frxp  6856  wfrlem12  6997  tz7.49  7112  dif1en  7752  enp1i  7754  frfi  7764  unblem3  7773  isfinite2  7777  iunfi  7810  tcrank  8302  infdif  8585  isf34lem6  8756  axdc3lem4  8829  suplem1pr  9423  uzwo  11168  gsumcom2  17545  cmpsublem  20351  nrmhaus  20778  metrest  21476  finiunmbl  22434  wilthlem3  23932  cusgrafi  25147  clwwlkn0  25439  h1datomi  27171  chirredlem1  27980  mclsax  30154  frrlem11  30472  lineext  30787  onsucconi  31041  sdclem2  31978  heibor1lem  32048  cotrintab  36134  tgblthelfgott  38721
  Copyright terms: Public domain W3C validator