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  2497  xpcan  6165  xpcan2  6166  sucdom2OLD  9094  mapxpen  9155  sucdom2  9215  f1finf1oOLD  9276  inf3lem3  9642  dfac12r  10159  nnadju  10210  cfsuc  10269  fin23lem26  10337  iundom2g  10552  inar1  10787  rankcf  10789  ltsrpr  11089  supsrlem  11123  axpre-sup  11181  nominpos  12476  ublbneg  12947  qbtwnre  13213  fsequb  13991  fi1uzind  14523  brfi1indALT  14526  ccats1pfxeqrex  14731  rexanre  15363  rexuzre  15369  rexico  15370  caubnd  15375  rlim2lt  15511  rlim3  15512  lo1bddrp  15539  o1lo1  15551  climshftlem  15588  rlimcn3  15604  rlimo1  15631  lo1add  15641  lo1mul  15642  lo1le  15666  isercoll  15682  serf0  15695  cvgcmp  15830  dvds1lem  16285  dvds2lem  16286  mulmoddvds  16347  isprm5  16724  vdwlem2  17000  vdwlem10  17008  vdwlem11  17009  lsmcv  21100  lmconst  23197  ptcnplem  23557  fclscmp  23966  tsmsres  24080  addcnlem  24802  lebnumlem3  24911  xlebnum  24913  lebnumii  24914  iscmet3lem2  25242  bcthlem4  25277  cniccbdd  25412  ovoliunlem2  25454  mbfi1flimlem  25673  ply1divex  26092  aalioulem3  26292  aalioulem5  26294  aalioulem6  26295  aaliou  26296  ulmshftlem  26348  ulmbdd  26357  tanarg  26578  cxploglim  26938  ftalem2  27034  ftalem7  27039  dchrisumlem3  27452  frgrogt3nreg  30324  ubthlem3  30799  spansncol  31495  riesz1  31992  fineqvac  35074  erdsze2lem2  35172  dfrdg4  35915  neibastop2  36325  onsuct0  36405  weiunpo  36429  bj-bary1  37276  topdifinffinlem  37311  finorwe  37346  poimirlem24  37614  incsequz  37718  caushft  37731  equivbnd  37760  cntotbnd  37766  4atexlemex4  40038  frege124d  43732  gneispace  44105  expgrowth  44307  vk15.4j  44501  sstrALT2  44807  iccpartdisj  47399  fppr2odd  47693