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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  dfsb2  2496  xpcan  6019  xpcan2  6020  sucdom2  8733  mapxpen  8790  f1finf1o  8880  unfiOLD  8916  inf3lem3  9223  dfac12r  9725  nnadju  9776  cfsuc  9836  fin23lem26  9904  iundom2g  10119  inar1  10354  rankcf  10356  ltsrpr  10656  supsrlem  10690  axpre-sup  10748  nominpos  12032  ublbneg  12494  qbtwnre  12754  fsequb  13513  fi1uzind  14028  brfi1indALT  14031  ccats1pfxeqrex  14245  rexanre  14875  rexuzre  14881  rexico  14882  caubnd  14887  rlim2lt  15023  rlim3  15024  lo1bddrp  15051  o1lo1  15063  climshftlem  15100  rlimcn3  15116  rlimo1  15143  lo1add  15153  lo1mul  15154  lo1le  15180  isercoll  15196  serf0  15209  cvgcmp  15343  dvds1lem  15792  dvds2lem  15793  mulmoddvds  15854  isprm5  16227  vdwlem2  16498  vdwlem10  16506  vdwlem11  16507  lsmcv  20132  lmconst  22112  ptcnplem  22472  fclscmp  22881  tsmsres  22995  addcnlem  23715  lebnumlem3  23814  xlebnum  23816  lebnumii  23817  iscmet3lem2  24143  bcthlem4  24178  cniccbdd  24312  ovoliunlem2  24354  mbfi1flimlem  24574  ply1divex  24988  aalioulem3  25181  aalioulem5  25183  aalioulem6  25184  aaliou  25185  ulmshftlem  25235  ulmbdd  25244  tanarg  25461  cxploglim  25814  ftalem2  25910  ftalem7  25915  dchrisumlem3  26326  frgrogt3nreg  28434  ubthlem3  28907  spansncol  29603  riesz1  30100  fineqvac  32733  erdsze2lem2  32833  dfrdg4  33939  neibastop2  34236  onsuct0  34316  bj-bary1  35166  topdifinffinlem  35204  finorwe  35239  poimirlem24  35487  incsequz  35592  caushft  35605  equivbnd  35634  cntotbnd  35640  4atexlemex4  37773  frege124d  40987  gneispace  41362  expgrowth  41567  vk15.4j  41762  sstrALT2  42069  iccpartdisj  44505  fppr2odd  44799