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  2380  dmcosseq  5253  iss  5309  funopg  5602  limuni3  6660  frxp  6883  tz7.49  7102  dif1en  7745  enp1i  7747  frfi  7757  unblem3  7766  isfinite2  7770  iunfi  7800  tcrank  8293  infdif  8580  isf34lem6  8751  axdc3lem4  8824  suplem1pr  9419  uzwo  11145  uzwoOLD  11146  gsumcom2  17202  cmpsublem  20069  nrmhaus  20496  metrest  21196  finiunmbl  22123  wilthlem3  23545  cusgrafi  24687  clwwlkn0  24979  h1datomi  26700  chirredlem1  27510  mclsax  29196  wfrlem12  29597  frrlem11  29642  lineext  29957  onsucconi  30133  sdclem2  30478  heibor1lem  30548
  Copyright terms: Public domain W3C validator