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  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