Theorem syl6an 683

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  2501  xpcan  6207  xpcan2  6208  sucdom2OLD  9148  mapxpen  9209  sucdom2  9269  f1finf1oOLD  9334  inf3lem3  9699  dfac12r  10216  nnadju  10267  cfsuc  10326  fin23lem26  10394  iundom2g  10609  inar1  10844  rankcf  10846  ltsrpr  11146  supsrlem  11180  axpre-sup  11238  nominpos  12530  ublbneg  12998  qbtwnre  13261  fsequb  14026  fi1uzind  14556  brfi1indALT  14559  ccats1pfxeqrex  14763  rexanre  15395  rexuzre  15401  rexico  15402  caubnd  15407  rlim2lt  15543  rlim3  15544  lo1bddrp  15571  o1lo1  15583  climshftlem  15620  rlimcn3  15636  rlimo1  15663  lo1add  15673  lo1mul  15674  lo1le  15700  isercoll  15716  serf0  15729  cvgcmp  15864  dvds1lem  16316  dvds2lem  16317  mulmoddvds  16378  isprm5  16754  vdwlem2  17029  vdwlem10  17037  vdwlem11  17038  lsmcv  21166  lmconst  23290  ptcnplem  23650  fclscmp  24059  tsmsres  24173  addcnlem  24905  lebnumlem3  25014  xlebnum  25016  lebnumii  25017  iscmet3lem2  25345  bcthlem4  25380  cniccbdd  25515  ovoliunlem2  25557  mbfi1flimlem  25777  ply1divex  26196  aalioulem3  26394  aalioulem5  26396  aalioulem6  26397  aaliou  26398  ulmshftlem  26450  ulmbdd  26459  tanarg  26679  cxploglim  27039  ftalem2  27135  ftalem7  27140  dchrisumlem3  27553  frgrogt3nreg  30429  ubthlem3  30904  spansncol  31600  riesz1  32097  fineqvac  35073  erdsze2lem2  35172  dfrdg4  35915  neibastop2  36327  onsuct0  36407  weiunpo  36431  bj-bary1  37278  topdifinffinlem  37313  finorwe  37348  poimirlem24  37604  incsequz  37708  caushft  37721  equivbnd  37750  cntotbnd  37756  4atexlemex4  40030  frege124d  43723  gneispace  44096  expgrowth  44304  vk15.4j  44499  sstrALT2  44806  iccpartdisj  47311  fppr2odd  47605