Theorem syl6com 35

Description: Syllogism inference with commuted antecedents. (Contributed by NM, 25-May-2005.)

Hypotheses

Ref	Expression
syl6com.1
syl6com.2

Assertion

Ref	Expression
syl6com

Proof of Theorem syl6com

Step	Hyp	Ref	Expression
1		syl6com.1	. . 3
2		syl6com.2	. . 3
3	1, 2	syl6 33	. 2
4	3	com12 31	1

Syntax hints:  ->wi 4

This theorem is referenced by:  19.33b  1696  ax6e  2002  axc16i  2064  rgen2a  2884  wefrc  4878  elres  5314  sorpssuni  6589  sorpssint  6590  ordzsl  6680  limuni3  6687  funcnvuni  6753  funrnex  6767  soxp  6913  oaabs  7312  eceqoveq  7435  php3  7723  pssinf  7750  unbnn2  7797  inf0  8059  inf3lem5  8070  tcel  8197  rankxpsuc  8321  carduni  8383  prdom2  8405  dfac5  8530  cflm  8651  indpi  9306  prlem934  9432  xrub  11532  injresinjlem  11925  hashgt12el  12481  hashgt12el2  12482  brfi1uzind  12532  cshwcsh2id  12796  cshwshash  14589  symgextf1  16446  gsummoncoe1  18346  basis2  19452  bwthOLD  19911  fbdmn0  20335  usgranloopv  24378  nbgranself2  24436  usgrnloop  24565  wlkdvspthlem  24609  4cyclusnfrgra  25019  frgrancvvdeqlem7  25036  rngoueqz  25432  atcv0eq  27298  dfon2lem9  29223  trpredrec  29321  frmin  29322  wfrlem4  29346  wfrlem12  29354  frrlem4  29390  frrlem11  29399  altopthsn  29611  rankeq1o  29828  wl-equsb4  30005  hbtlem5  31077  funressnfv  32213  afvco2  32261  ndmaovcl  32288  rngdir  32688  zlmodzxznm  33098

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