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  5212  iss  5265  funopg  5561  limuni3  6576  frxp  6795  tz7.49  7013  dif1enOLD  7658  dif1en  7659  enp1i  7661  frfi  7671  unblem3  7680  isfinite2  7684  iunfi  7713  tcrank  8206  infdif  8493  isf34lem6  8664  axdc3lem4  8737  suplem1pr  9336  uzwo  11032  uzwoOLD  11033  gsumcom2  16599  cmpsublem  19144  nrmhaus  19541  metrest  20241  finiunmbl  21168  wilthlem3  22551  cusgrafi  23569  h1datomi  25163  chirredlem1  25973  wfrlem12  27902  frrlem11  27947  lineext  28274  onsucconi  28450  sdclem2  28809  heibor1lem  28879  clwwlkn0  30608
  Copyright terms: Public domain W3C validator