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  2491  xpcan  6149  xpcan2  6150  mapxpen  9107  sucdom2  9167  f1finf1oOLD  9217  inf3lem3  9583  dfac12r  10100  nnadju  10151  cfsuc  10210  fin23lem26  10278  iundom2g  10493  inar1  10728  rankcf  10730  ltsrpr  11030  supsrlem  11064  axpre-sup  11122  nominpos  12419  ublbneg  12892  qbtwnre  13159  fsequb  13940  fi1uzind  14472  brfi1indALT  14475  ccats1pfxeqrex  14680  rexanre  15313  rexuzre  15319  rexico  15320  caubnd  15325  rlim2lt  15463  rlim3  15464  lo1bddrp  15491  o1lo1  15503  climshftlem  15540  rlimcn3  15556  rlimo1  15583  lo1add  15593  lo1mul  15594  lo1le  15618  isercoll  15634  serf0  15647  cvgcmp  15782  dvds1lem  16237  dvds2lem  16238  mulmoddvds  16300  isprm5  16677  vdwlem2  16953  vdwlem10  16961  vdwlem11  16962  lsmcv  21051  lmconst  23148  ptcnplem  23508  fclscmp  23917  tsmsres  24031  addcnlem  24753  lebnumlem3  24862  xlebnum  24864  lebnumii  24865  iscmet3lem2  25192  bcthlem4  25227  cniccbdd  25362  ovoliunlem2  25404  mbfi1flimlem  25623  ply1divex  26042  aalioulem3  26242  aalioulem5  26244  aalioulem6  26245  aaliou  26246  ulmshftlem  26298  ulmbdd  26307  tanarg  26528  cxploglim  26888  ftalem2  26984  ftalem7  26989  dchrisumlem3  27402  frgrogt3nreg  30326  ubthlem3  30801  spansncol  31497  riesz1  31994  fineqvac  35087  erdsze2lem2  35191  dfrdg4  35939  neibastop2  36349  onsuct0  36429  weiunpo  36453  bj-bary1  37300  topdifinffinlem  37335  finorwe  37370  poimirlem24  37638  incsequz  37742  caushft  37755  equivbnd  37784  cntotbnd  37790  4atexlemex4  40067  frege124d  43750  gneispace  44123  expgrowth  44324  vk15.4j  44518  sstrALT2  44824  iccpartdisj  47438  fppr2odd  47732