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  2492  xpcan  6152  xpcan2  6153  sucdom2OLD  9056  mapxpen  9113  sucdom2  9173  f1finf1oOLD  9224  inf3lem3  9590  dfac12r  10107  nnadju  10158  cfsuc  10217  fin23lem26  10285  iundom2g  10500  inar1  10735  rankcf  10737  ltsrpr  11037  supsrlem  11071  axpre-sup  11129  nominpos  12426  ublbneg  12899  qbtwnre  13166  fsequb  13947  fi1uzind  14479  brfi1indALT  14482  ccats1pfxeqrex  14687  rexanre  15320  rexuzre  15326  rexico  15327  caubnd  15332  rlim2lt  15470  rlim3  15471  lo1bddrp  15498  o1lo1  15510  climshftlem  15547  rlimcn3  15563  rlimo1  15590  lo1add  15600  lo1mul  15601  lo1le  15625  isercoll  15641  serf0  15654  cvgcmp  15789  dvds1lem  16244  dvds2lem  16245  mulmoddvds  16307  isprm5  16684  vdwlem2  16960  vdwlem10  16968  vdwlem11  16969  lsmcv  21058  lmconst  23155  ptcnplem  23515  fclscmp  23924  tsmsres  24038  addcnlem  24760  lebnumlem3  24869  xlebnum  24871  lebnumii  24872  iscmet3lem2  25199  bcthlem4  25234  cniccbdd  25369  ovoliunlem2  25411  mbfi1flimlem  25630  ply1divex  26049  aalioulem3  26249  aalioulem5  26251  aalioulem6  26252  aaliou  26253  ulmshftlem  26305  ulmbdd  26314  tanarg  26535  cxploglim  26895  ftalem2  26991  ftalem7  26996  dchrisumlem3  27409  frgrogt3nreg  30333  ubthlem3  30808  spansncol  31504  riesz1  32001  fineqvac  35094  erdsze2lem2  35198  dfrdg4  35946  neibastop2  36356  onsuct0  36436  weiunpo  36460  bj-bary1  37307  topdifinffinlem  37342  finorwe  37377  poimirlem24  37645  incsequz  37749  caushft  37762  equivbnd  37791  cntotbnd  37797  4atexlemex4  40074  frege124d  43757  gneispace  44130  expgrowth  44331  vk15.4j  44525  sstrALT2  44831  iccpartdisj  47442  fppr2odd  47736