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

Theorem sylcom 29
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 13 . 2  |-  ( ( ps  ->  ch )  ->  ( ps  ->  th )
)
41, 3syl 16 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  30  syl6  33  syli  37  mpbidi  216  2eu6  2393  dmcosseq  5270  iss  5327  funopg  5626  limuni3  6682  frxp  6905  tz7.49  7122  dif1enOLD  7764  dif1en  7765  enp1i  7767  frfi  7777  unblem3  7786  isfinite2  7790  iunfi  7820  tcrank  8314  infdif  8601  isf34lem6  8772  axdc3lem4  8845  suplem1pr  9442  uzwo  11156  uzwoOLD  11157  gsumcom2  16876  cmpsublem  19767  nrmhaus  20195  metrest  20895  finiunmbl  21822  wilthlem3  23210  cusgrafi  24305  clwwlkn0  24597  h1datomi  26322  chirredlem1  27132  wfrlem12  29281  frrlem11  29326  lineext  29653  onsucconi  29829  sdclem2  30162  heibor1lem  30232
  Copyright terms: Public domain W3C validator