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  2383  dmcosseq  5269  iss  5326  funopg  5625  limuni3  6687  frxp  6910  tz7.49  7129  dif1enOLD  7772  dif1en  7773  enp1i  7775  frfi  7785  unblem3  7794  isfinite2  7798  iunfi  7828  tcrank  8323  infdif  8610  isf34lem6  8781  axdc3lem4  8854  suplem1pr  9451  uzwo  11173  uzwoOLD  11174  gsumcom2  17003  cmpsublem  19899  nrmhaus  20327  metrest  21027  finiunmbl  21954  wilthlem3  23344  cusgrafi  24482  clwwlkn0  24774  h1datomi  26499  chirredlem1  27309  mclsax  28929  wfrlem12  29354  frrlem11  29399  lineext  29726  onsucconi  29902  sdclem2  30235  heibor1lem  30305 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
 Copyright terms: Public domain W3C validator