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  6135  xpcan2  6136  mapxpen  9075  sucdom2  9131  inf3lem3  9543  dfac12r  10061  nnadju  10112  cfsuc  10171  fin23lem26  10239  iundom2g  10454  inar1  10690  rankcf  10692  ltsrpr  10992  supsrlem  11026  axpre-sup  11084  nominpos  12382  ublbneg  12850  qbtwnre  13118  fsequb  13902  fi1uzind  14434  brfi1indALT  14437  ccats1pfxeqrex  14642  rexanre  15274  rexuzre  15280  rexico  15281  caubnd  15286  rlim2lt  15424  rlim3  15425  lo1bddrp  15452  o1lo1  15464  climshftlem  15501  rlimcn3  15517  rlimo1  15544  lo1add  15554  lo1mul  15555  lo1le  15579  isercoll  15595  serf0  15608  cvgcmp  15743  dvds1lem  16198  dvds2lem  16199  mulmoddvds  16261  isprm5  16638  vdwlem2  16914  vdwlem10  16922  vdwlem11  16923  lsmcv  21100  lmconst  23209  ptcnplem  23569  fclscmp  23978  tsmsres  24092  addcnlem  24813  lebnumlem3  24922  xlebnum  24924  lebnumii  24925  iscmet3lem2  25252  bcthlem4  25287  cniccbdd  25422  ovoliunlem2  25464  mbfi1flimlem  25683  ply1divex  26102  aalioulem3  26302  aalioulem5  26304  aalioulem6  26305  aaliou  26306  ulmshftlem  26358  ulmbdd  26367  tanarg  26588  cxploglim  26948  ftalem2  27044  ftalem7  27049  dchrisumlem3  27462  frgrogt3nreg  30455  ubthlem3  30930  spansncol  31626  riesz1  32123  fineqvac  35253  erdsze2lem2  35379  dfrdg4  36126  neibastop2  36536  onsuct0  36616  weiunpo  36640  bj-bary1  37488  topdifinffinlem  37523  finorwe  37558  poimirlem24  37816  incsequz  37920  caushft  37933  equivbnd  37962  cntotbnd  37968  4atexlemex4  40370  frege124d  44038  gneispace  44411  expgrowth  44612  vk15.4j  44805  sstrALT2  45111  iccpartdisj  47719  fppr2odd  48013