MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylcom Structured version   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  sbequi  2136  limuni3  4824  dmcosseq  5129  iss  5181  funopg  5477  frxp  6448  tz7.49  6694  abianfp  6708  dif1enOLD  7332  dif1en  7333  enp1i  7335  frfi  7344  unblem3  7353  isfinite2  7357  iunfi  7386  tcrank  7800  infdif  8081  isf34lem6  8252  axdc3lem4  8325  suplem1pr  8921  uzwo  10531  uzwoOLD  10532  gsumcom2  15541  cmpsublem  17454  nrmhaus  17850  metrest  18546  finiunmbl  19430  wilthlem3  20845  cusgrafi  21483  h1datomi  23075  chirredlem1  23885  wfrlem12  25541  frrlem11  25586  lineext  26002  onsucconi  26179  sdclem2  26437  heibor1lem  26509
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator