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  2498  xpcan  6196  xpcan2  6197  sucdom2OLD  9122  mapxpen  9183  sucdom2  9243  f1finf1oOLD  9306  inf3lem3  9670  dfac12r  10187  nnadju  10238  cfsuc  10297  fin23lem26  10365  iundom2g  10580  inar1  10815  rankcf  10817  ltsrpr  11117  supsrlem  11151  axpre-sup  11209  nominpos  12503  ublbneg  12975  qbtwnre  13241  fsequb  14016  fi1uzind  14546  brfi1indALT  14549  ccats1pfxeqrex  14753  rexanre  15385  rexuzre  15391  rexico  15392  caubnd  15397  rlim2lt  15533  rlim3  15534  lo1bddrp  15561  o1lo1  15573  climshftlem  15610  rlimcn3  15626  rlimo1  15653  lo1add  15663  lo1mul  15664  lo1le  15688  isercoll  15704  serf0  15717  cvgcmp  15852  dvds1lem  16305  dvds2lem  16306  mulmoddvds  16367  isprm5  16744  vdwlem2  17020  vdwlem10  17028  vdwlem11  17029  lsmcv  21143  lmconst  23269  ptcnplem  23629  fclscmp  24038  tsmsres  24152  addcnlem  24886  lebnumlem3  24995  xlebnum  24997  lebnumii  24998  iscmet3lem2  25326  bcthlem4  25361  cniccbdd  25496  ovoliunlem2  25538  mbfi1flimlem  25757  ply1divex  26176  aalioulem3  26376  aalioulem5  26378  aalioulem6  26379  aaliou  26380  ulmshftlem  26432  ulmbdd  26441  tanarg  26661  cxploglim  27021  ftalem2  27117  ftalem7  27122  dchrisumlem3  27535  frgrogt3nreg  30416  ubthlem3  30891  spansncol  31587  riesz1  32084  fineqvac  35111  erdsze2lem2  35209  dfrdg4  35952  neibastop2  36362  onsuct0  36442  weiunpo  36466  bj-bary1  37313  topdifinffinlem  37348  finorwe  37383  poimirlem24  37651  incsequz  37755  caushft  37768  equivbnd  37797  cntotbnd  37803  4atexlemex4  40075  frege124d  43774  gneispace  44147  expgrowth  44354  vk15.4j  44548  sstrALT2  44855  iccpartdisj  47424  fppr2odd  47718