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

Step	Hyp	Ref	Expression
1		sylcom.1	. 2
2		sylcom.2	. . 3
3	2	a2i 13	. 2
4	1, 3	syl 16	1

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