Theorem syl6an 684

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.1	. 2 ⊢ (𝜑 → 𝜓)
2		syl6an.2	. 2 ⊢ (𝜑 → (𝜒 → 𝜃))
3		syl6an.3	. . 3 ⊢ ((𝜓 ∧ 𝜃) → 𝜏)
4	3	ex 412	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	1, 2, 4	sylsyld 61	1 ⊢ (𝜑 → (𝜒 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  dfsb2  2495  xpcan  6197  xpcan2  6198  sucdom2OLD  9120  mapxpen  9181  sucdom2  9240  f1finf1oOLD  9303  inf3lem3  9667  dfac12r  10184  nnadju  10235  cfsuc  10294  fin23lem26  10362  iundom2g  10577  inar1  10812  rankcf  10814  ltsrpr  11114  supsrlem  11148  axpre-sup  11206  nominpos  12500  ublbneg  12972  qbtwnre  13237  fsequb  14012  fi1uzind  14542  brfi1indALT  14545  ccats1pfxeqrex  14749  rexanre  15381  rexuzre  15387  rexico  15388  caubnd  15393  rlim2lt  15529  rlim3  15530  lo1bddrp  15557  o1lo1  15569  climshftlem  15606  rlimcn3  15622  rlimo1  15649  lo1add  15659  lo1mul  15660  lo1le  15684  isercoll  15700  serf0  15713  cvgcmp  15848  dvds1lem  16301  dvds2lem  16302  mulmoddvds  16363  isprm5  16740  vdwlem2  17015  vdwlem10  17023  vdwlem11  17024  lsmcv  21160  lmconst  23284  ptcnplem  23644  fclscmp  24053  tsmsres  24167  addcnlem  24899  lebnumlem3  25008  xlebnum  25010  lebnumii  25011  iscmet3lem2  25339  bcthlem4  25374  cniccbdd  25509  ovoliunlem2  25551  mbfi1flimlem  25771  ply1divex  26190  aalioulem3  26390  aalioulem5  26392  aalioulem6  26393  aaliou  26394  ulmshftlem  26446  ulmbdd  26455  tanarg  26675  cxploglim  27035  ftalem2  27131  ftalem7  27136  dchrisumlem3  27549  frgrogt3nreg  30425  ubthlem3  30900  spansncol  31596  riesz1  32093  fineqvac  35089  erdsze2lem2  35188  dfrdg4  35932  neibastop2  36343  onsuct0  36423  weiunpo  36447  bj-bary1  37294  topdifinffinlem  37329  finorwe  37364  poimirlem24  37630  incsequz  37734  caushft  37747  equivbnd  37776  cntotbnd  37782  4atexlemex4  40055  frege124d  43750  gneispace  44123  expgrowth  44330  vk15.4j  44525  sstrALT2  44832  iccpartdisj  47361  fppr2odd  47655