Theorem syl6an 681

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  dfsb2  2497  xpcan  6079  xpcan2  6080  sucdom2OLD  8869  mapxpen  8930  sucdom2  8989  f1finf1o  9046  unfiOLD  9081  inf3lem3  9388  dfac12r  9902  nnadju  9953  cfsuc  10013  fin23lem26  10081  iundom2g  10296  inar1  10531  rankcf  10533  ltsrpr  10833  supsrlem  10867  axpre-sup  10925  nominpos  12210  ublbneg  12673  qbtwnre  12933  fsequb  13695  fi1uzind  14211  brfi1indALT  14214  ccats1pfxeqrex  14428  rexanre  15058  rexuzre  15064  rexico  15065  caubnd  15070  rlim2lt  15206  rlim3  15207  lo1bddrp  15234  o1lo1  15246  climshftlem  15283  rlimcn3  15299  rlimo1  15326  lo1add  15336  lo1mul  15337  lo1le  15363  isercoll  15379  serf0  15392  cvgcmp  15528  dvds1lem  15977  dvds2lem  15978  mulmoddvds  16039  isprm5  16412  vdwlem2  16683  vdwlem10  16691  vdwlem11  16692  lsmcv  20403  lmconst  22412  ptcnplem  22772  fclscmp  23181  tsmsres  23295  addcnlem  24027  lebnumlem3  24126  xlebnum  24128  lebnumii  24129  iscmet3lem2  24456  bcthlem4  24491  cniccbdd  24625  ovoliunlem2  24667  mbfi1flimlem  24887  ply1divex  25301  aalioulem3  25494  aalioulem5  25496  aalioulem6  25497  aaliou  25498  ulmshftlem  25548  ulmbdd  25557  tanarg  25774  cxploglim  26127  ftalem2  26223  ftalem7  26228  dchrisumlem3  26639  frgrogt3nreg  28761  ubthlem3  29234  spansncol  29930  riesz1  30427  fineqvac  33066  erdsze2lem2  33166  dfrdg4  34253  neibastop2  34550  onsuct0  34630  bj-bary1  35483  topdifinffinlem  35518  finorwe  35553  poimirlem24  35801  incsequz  35906  caushft  35919  equivbnd  35948  cntotbnd  35954  4atexlemex4  38087  frege124d  41369  gneispace  41744  expgrowth  41953  vk15.4j  42148  sstrALT2  42455  iccpartdisj  44889  fppr2odd  45183