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  6141  xpcan2  6142  mapxpen  9081  sucdom2  9137  inf3lem3  9551  dfac12r  10069  nnadju  10120  cfsuc  10179  fin23lem26  10247  iundom2g  10462  inar1  10698  rankcf  10700  ltsrpr  11000  supsrlem  11034  axpre-sup  11092  nominpos  12414  ublbneg  12883  qbtwnre  13151  fsequb  13937  fi1uzind  14469  brfi1indALT  14472  ccats1pfxeqrex  14677  rexanre  15309  rexuzre  15315  rexico  15316  caubnd  15321  rlim2lt  15459  rlim3  15460  lo1bddrp  15487  o1lo1  15499  climshftlem  15536  rlimcn3  15552  rlimo1  15579  lo1add  15589  lo1mul  15590  lo1le  15614  isercoll  15630  serf0  15643  cvgcmp  15779  dvds1lem  16236  dvds2lem  16237  mulmoddvds  16299  isprm5  16677  vdwlem2  16953  vdwlem10  16961  vdwlem11  16962  lsmcv  21139  lmconst  23226  ptcnplem  23586  fclscmp  23995  tsmsres  24109  addcnlem  24830  lebnumlem3  24930  xlebnum  24932  lebnumii  24933  iscmet3lem2  25259  bcthlem4  25294  cniccbdd  25428  ovoliunlem2  25470  mbfi1flimlem  25689  ply1divex  26102  aalioulem3  26300  aalioulem5  26302  aalioulem6  26303  aaliou  26304  ulmshftlem  26354  ulmbdd  26363  tanarg  26583  cxploglim  26941  ftalem2  27037  ftalem7  27042  dchrisumlem3  27454  frgrogt3nreg  30467  ubthlem3  30943  spansncol  31639  riesz1  32136  fineqvac  35260  erdsze2lem2  35386  dfrdg4  36133  neibastop2  36543  onsuct0  36623  weiunpo  36647  bj-bary1  37626  topdifinffinlem  37663  finorwe  37698  poimirlem24  37965  incsequz  38069  caushft  38082  equivbnd  38111  cntotbnd  38117  4atexlemex4  40519  frege124d  44188  gneispace  44561  expgrowth  44762  vk15.4j  44955  sstrALT2  45261  iccpartdisj  47891  fppr2odd  48201