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 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  dmcosseq  5090  iss  5144  funopg  5440  limuni3  6454  frxp  6673  tz7.49  6888  abianfp  6902  dif1enOLD  7534  dif1en  7535  enp1i  7537  frfi  7547  unblem3  7556  isfinite2  7560  iunfi  7589  tcrank  8081  infdif  8368  isf34lem6  8539  axdc3lem4  8612  suplem1pr  9211  uzwo  10907  uzwoOLD  10908  gsumcom2  16443  cmpsublem  18846  nrmhaus  19243  metrest  19943  finiunmbl  20869  wilthlem3  22295  cusgrafi  23215  h1datomi  24809  chirredlem1  25619  wfrlem12  27584  frrlem11  27629  lineext  27956  onsucconi  28133  sdclem2  28484  heibor1lem  28554  clwwlkn0  30285
  Copyright terms: Public domain W3C validator