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

Theorem sylcom 27
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 set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl5com  28  syl6  31  syli  35  mpbidi  208  limuni3  4773  dmcosseq  5078  iss  5130  funopg  5426  frxp  6393  tz7.49  6639  abianfp  6653  dif1enOLD  7277  dif1en  7278  enp1i  7280  frfi  7289  unblem3  7298  isfinite2  7302  iunfi  7331  tcrank  7742  infdif  8023  isf34lem6  8194  axdc3lem4  8267  suplem1pr  8863  uzwo  10472  uzwoOLD  10473  gsumcom2  15477  cmpsublem  17385  nrmhaus  17780  metrest  18445  finiunmbl  19306  wilthlem3  20721  cusgrafi  21358  h1datomi  22932  chirredlem1  23742  wfrlem12  25292  frrlem11  25318  lineext  25725  onsucconi  25902  sdclem2  26138  heibor1lem  26210
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator