Theorem syl6an 682

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  dfsb2  2532  dfsb2ALT  2591  xpcan  6033  xpcan2  6034  mapxpen  8683  sucdom2  8714  f1finf1o  8745  unfi  8785  inf3lem3  9093  dfac12r  9572  cfsuc  9679  fin23lem26  9747  iundom2g  9962  inar1  10197  rankcf  10199  ltsrpr  10499  supsrlem  10533  axpre-sup  10591  nominpos  11875  ublbneg  12334  qbtwnre  12593  fsequb  13344  fi1uzind  13856  brfi1indALT  13859  ccats1pfxeqrex  14077  rexanre  14706  rexuzre  14712  rexico  14713  caubnd  14718  rlim2lt  14854  rlim3  14855  lo1bddrp  14882  o1lo1  14894  climshftlem  14931  rlimcn2  14947  rlimo1  14973  lo1add  14983  lo1mul  14984  lo1le  15008  isercoll  15024  serf0  15037  cvgcmp  15171  dvds1lem  15621  dvds2lem  15622  mulmoddvds  15679  isprm5  16051  vdwlem2  16318  vdwlem10  16326  vdwlem11  16327  lsmcv  19913  lmconst  21869  ptcnplem  22229  fclscmp  22638  tsmsres  22752  addcnlem  23472  lebnumlem3  23567  xlebnum  23569  lebnumii  23570  iscmet3lem2  23895  bcthlem4  23930  cniccbdd  24062  ovoliunlem2  24104  mbfi1flimlem  24323  ply1divex  24730  aalioulem3  24923  aalioulem5  24925  aalioulem6  24926  aaliou  24927  ulmshftlem  24977  ulmbdd  24986  tanarg  25202  cxploglim  25555  ftalem2  25651  ftalem7  25656  dchrisumlem3  26067  frgrogt3nreg  28176  ubthlem3  28649  spansncol  29345  riesz1  29842  erdsze2lem2  32451  dfrdg4  33412  neibastop2  33709  onsuct0  33789  bj-bary1  34596  topdifinffinlem  34631  finorwe  34666  poimirlem24  34931  incsequz  35038  caushft  35051  equivbnd  35083  cntotbnd  35089  4atexlemex4  37224  frege124d  40126  gneispace  40504  expgrowth  40687  vk15.4j  40882  sstrALT2  41189  iccpartdisj  43617  fppr2odd  43916