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  4659  dmcosseq  4962  iss  5014  funopg  5302  frxp  6241  tz7.49  6473  abianfp  6487  dif1enOLD  7106  dif1en  7107  enp1i  7109  frfi  7118  unblem3  7127  isfinite2  7131  iunfi  7160  tcrank  7570  infdif  7851  isf34lem6  8022  axdc3lem4  8095  suplem1pr  8692  uzwo  10297  uzwoOLD  10298  gsumcom2  15242  cmpsublem  17142  nrmhaus  17533  metrest  18086  finiunmbl  18917  wilthlem3  20324  h1datomi  22176  chirredlem1  22986  wfrlem12  24338  frrlem11  24364  lineext  24771  onsucconi  24948  sdclem2  26555  heibor1lem  26636
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator