Theorem sylcom 28

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
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  29  syl6  32  syli  36  mpbidi  210  dmcosseq  5072  iss  5126  funopg  5422  limuni3  6433  frxp  6651  tz7.49  6859  abianfp  6873  dif1enOLD  7503  dif1en  7504  enp1i  7506  frfi  7516  unblem3  7525  isfinite2  7529  iunfi  7558  tcrank  8038  infdif  8325  isf34lem6  8496  axdc3lem4  8569  suplem1pr  9167  uzwo  10862  uzwoOLD  10863  gsumcom2  16358  cmpsublem  18706  nrmhaus  19103  metrest  19799  finiunmbl  20725  wilthlem3  22149  cusgrafi  23069  h1datomi  24663  chirredlem1  25473  wfrlem12  27437  frrlem11  27482  lineext  27809  onsucconi  27986  sdclem2  28309  heibor1lem  28379  clwwlkn0  30111  gsumXcom2  30507

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7