Theorem syl6an 685

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  2498  xpcan  6132  xpcan2  6133  mapxpen  9072  sucdom2  9128  inf3lem3  9540  dfac12r  10058  nnadju  10109  cfsuc  10168  fin23lem26  10236  iundom2g  10451  inar1  10687  rankcf  10689  ltsrpr  10989  supsrlem  11023  axpre-sup  11081  nominpos  12403  ublbneg  12872  qbtwnre  13140  fsequb  13926  fi1uzind  14458  brfi1indALT  14461  ccats1pfxeqrex  14666  rexanre  15298  rexuzre  15304  rexico  15305  caubnd  15310  rlim2lt  15448  rlim3  15449  lo1bddrp  15476  o1lo1  15488  climshftlem  15525  rlimcn3  15541  rlimo1  15568  lo1add  15578  lo1mul  15579  lo1le  15603  isercoll  15619  serf0  15632  cvgcmp  15768  dvds1lem  16225  dvds2lem  16226  mulmoddvds  16288  isprm5  16666  vdwlem2  16942  vdwlem10  16950  vdwlem11  16951  lsmcv  21129  lmconst  23235  ptcnplem  23595  fclscmp  24004  tsmsres  24118  addcnlem  24839  lebnumlem3  24939  xlebnum  24941  lebnumii  24942  iscmet3lem2  25268  bcthlem4  25303  cniccbdd  25437  ovoliunlem2  25479  mbfi1flimlem  25698  ply1divex  26114  aalioulem3  26313  aalioulem5  26315  aalioulem6  26316  aaliou  26317  ulmshftlem  26369  ulmbdd  26378  tanarg  26599  cxploglim  26959  ftalem2  27055  ftalem7  27060  dchrisumlem3  27473  frgrogt3nreg  30487  ubthlem3  30963  spansncol  31659  riesz1  32156  fineqvac  35281  erdsze2lem2  35407  dfrdg4  36154  neibastop2  36564  onsuct0  36644  weiunpo  36668  bj-bary1  37639  topdifinffinlem  37674  finorwe  37709  poimirlem24  37976  incsequz  38080  caushft  38093  equivbnd  38122  cntotbnd  38128  4atexlemex4  40530  frege124d  44203  gneispace  44576  expgrowth  44777  vk15.4j  44970  sstrALT2  45276  iccpartdisj  47894  fppr2odd  48204