Theorem syl6an 545

Description: A syllogism deduction combined with conjoining antecedents. (Contributed by Alan Sare, 28-Oct-2011.)

Hypotheses

Ref	Expression
syl6an.1
syl6an.2
syl6an.3

Assertion

Ref	Expression
syl6an

Proof of Theorem syl6an

Step	Hyp	Ref	Expression
1		syl6an.2	. . 3
2		syl6an.1	. . 3
3	1, 2	jctild 543	. 2
4		syl6an.3	. 2
5	3, 4	syl6 33	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  dfsb2  2114  xpcan  5448  xpcan2  5449  mapxpen  7703  sucdom2  7734  f1finf1o  7766  unfi  7807  inf3lem3  8068  dfac12r  8547  cfsuc  8658  fin23lem26  8726  iundom2g  8936  inar1  9174  rankcf  9176  ltsrpr  9475  supsrlem  9509  axpre-sup  9567  infmrcl  10547  nominpos  10800  ublbneg  11195  qbtwnre  11427  fsequb  12085  brfi1uzind  12532  rexanre  13179  rexuzre  13185  rexico  13186  caubnd  13191  rlim2lt  13320  rlim3  13321  lo1bddrp  13348  o1lo1  13360  climshftlem  13397  rlimcn2  13413  rlimo1  13439  lo1add  13449  lo1mul  13450  lo1le  13474  isercoll  13490  serf0  13503  cvgcmp  13630  dvds1lem  13995  dvds2lem  13996  isprm5  14253  vdwlem2  14500  vdwlem10  14508  vdwlem11  14509  lsmcv  17787  lmconst  19762  ptcnplem  20122  fclscmp  20531  tsmsresOLD  20645  tsmsres  20646  addcnlem  21368  lebnumlem3  21463  xlebnum  21465  lebnumii  21466  iscmet3lem2  21731  bcthlem4  21766  cniccbdd  21873  ovoliunlem2  21914  mbfi1flimlem  22129  ply1divex  22537  aalioulem3  22730  aalioulem5  22732  aalioulem6  22733  aaliou  22734  ulmshftlem  22784  ulmbdd  22793  tanarg  23004  cxploglim  23307  ftalem2  23347  ftalem7  23352  dchrisumlem3  23676  nvnencycllem  24643  frgraogt3nreg  25120  ubthlem3  25788  spansncol  26486  riesz1  26984  erdsze2lem2  28648  dfrdg4  29600  onsuct0  29906  neibastop2  30179  incsequz  30241  caushft  30254  equivbnd  30286  cntotbnd  30292  expgrowth  31240  vk15.4j  33298  sstrALT2  33635  bj-bary1  34681  4atexlemex4  35797

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

This theorem depends on definitions:  df-bi 185  df-an 371