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  6131  xpcan2  6132  mapxpen  9066  sucdom2  9122  inf3lem3  9530  dfac12r  10048  nnadju  10099  cfsuc  10158  fin23lem26  10226  iundom2g  10441  inar1  10676  rankcf  10678  ltsrpr  10978  supsrlem  11012  axpre-sup  11070  nominpos  12368  ublbneg  12841  qbtwnre  13108  fsequb  13892  fi1uzind  14424  brfi1indALT  14427  ccats1pfxeqrex  14632  rexanre  15264  rexuzre  15270  rexico  15271  caubnd  15276  rlim2lt  15414  rlim3  15415  lo1bddrp  15442  o1lo1  15454  climshftlem  15491  rlimcn3  15507  rlimo1  15534  lo1add  15544  lo1mul  15545  lo1le  15569  isercoll  15585  serf0  15598  cvgcmp  15733  dvds1lem  16188  dvds2lem  16189  mulmoddvds  16251  isprm5  16628  vdwlem2  16904  vdwlem10  16912  vdwlem11  16913  lsmcv  21088  lmconst  23186  ptcnplem  23546  fclscmp  23955  tsmsres  24069  addcnlem  24790  lebnumlem3  24899  xlebnum  24901  lebnumii  24902  iscmet3lem2  25229  bcthlem4  25264  cniccbdd  25399  ovoliunlem2  25441  mbfi1flimlem  25660  ply1divex  26079  aalioulem3  26279  aalioulem5  26281  aalioulem6  26282  aaliou  26283  ulmshftlem  26335  ulmbdd  26344  tanarg  26565  cxploglim  26925  ftalem2  27021  ftalem7  27026  dchrisumlem3  27439  frgrogt3nreg  30388  ubthlem3  30863  spansncol  31559  riesz1  32056  fineqvac  35150  erdsze2lem2  35259  dfrdg4  36006  neibastop2  36416  onsuct0  36496  weiunpo  36520  bj-bary1  37367  topdifinffinlem  37402  finorwe  37437  poimirlem24  37694  incsequz  37798  caushft  37811  equivbnd  37840  cntotbnd  37846  4atexlemex4  40182  frege124d  43868  gneispace  44241  expgrowth  44442  vk15.4j  44635  sstrALT2  44941  iccpartdisj  47551  fppr2odd  47845