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

Theorem sylcom 25
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 12 . 2  |-  ( ( ps  ->  ch )  ->  ( ps  ->  th )
)
41, 3syl 15 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  syl5com  26  syl6  29  syli  33  mpbidi  207  limuni3  4643  dmcosseq  4946  iss  4998  funopg  5286  frxp  6225  tz7.49  6457  abianfp  6471  dif1enOLD  7090  dif1en  7091  enp1i  7093  frfi  7102  unblem3  7111  isfinite2  7115  iunfi  7144  tcrank  7554  infdif  7835  isf34lem6  8006  axdc3lem4  8079  suplem1pr  8676  uzwo  10281  uzwoOLD  10282  gsumcom2  15226  cmpsublem  17126  nrmhaus  17517  metrest  18070  finiunmbl  18901  wilthlem3  20308  h1datomi  22160  chirredlem1  22970  wfrlem12  24267  frrlem11  24293  lineext  24699  onsucconi  24876  sdclem2  26452  heibor1lem  26533
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator