MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylcom 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
sylcom.2
Assertion
Ref Expression
sylcom

Proof of Theorem sylcom
StepHypRef Expression
1 sylcom.1 . 2
2 sylcom.2 . . 3
32a2i 13 . 2
41, 3syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  syl5com  30  syl6  33  syli  37  mpbidi  216  2eu6  2380  dmcosseq  5218  iss  5272  funopg  5569  limuni3  6596  frxp  6816  tz7.49  7034  dif1enOLD  7679  dif1en  7680  enp1i  7682  frfi  7692  unblem3  7701  isfinite2  7705  iunfi  7734  tcrank  8228  infdif  8515  isf34lem6  8686  axdc3lem4  8759  suplem1pr  9358  uzwo  11056  uzwoOLD  11057  gsumcom2  16636  cmpsublem  19401  nrmhaus  19798  metrest  20498  finiunmbl  21425  wilthlem3  22808  cusgrafi  23859  h1datomi  25453  chirredlem1  26263  wfrlem12  28191  frrlem11  28236  lineext  28563  onsucconi  28739  sdclem2  29098  heibor1lem  29168  clwwlkn0  31314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator