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  6120  xpcan2  6121  mapxpen  9051  sucdom2  9107  inf3lem3  9515  dfac12r  10030  nnadju  10081  cfsuc  10140  fin23lem26  10208  iundom2g  10423  inar1  10658  rankcf  10660  ltsrpr  10960  supsrlem  10994  axpre-sup  11052  nominpos  12350  ublbneg  12823  qbtwnre  13090  fsequb  13874  fi1uzind  14406  brfi1indALT  14409  ccats1pfxeqrex  14614  rexanre  15246  rexuzre  15252  rexico  15253  caubnd  15258  rlim2lt  15396  rlim3  15397  lo1bddrp  15424  o1lo1  15436  climshftlem  15473  rlimcn3  15489  rlimo1  15516  lo1add  15526  lo1mul  15527  lo1le  15551  isercoll  15567  serf0  15580  cvgcmp  15715  dvds1lem  16170  dvds2lem  16171  mulmoddvds  16233  isprm5  16610  vdwlem2  16886  vdwlem10  16894  vdwlem11  16895  lsmcv  21071  lmconst  23169  ptcnplem  23529  fclscmp  23938  tsmsres  24052  addcnlem  24773  lebnumlem3  24882  xlebnum  24884  lebnumii  24885  iscmet3lem2  25212  bcthlem4  25247  cniccbdd  25382  ovoliunlem2  25424  mbfi1flimlem  25643  ply1divex  26062  aalioulem3  26262  aalioulem5  26264  aalioulem6  26265  aaliou  26266  ulmshftlem  26318  ulmbdd  26327  tanarg  26548  cxploglim  26908  ftalem2  27004  ftalem7  27009  dchrisumlem3  27422  frgrogt3nreg  30367  ubthlem3  30842  spansncol  31538  riesz1  32035  fineqvac  35107  erdsze2lem2  35216  dfrdg4  35964  neibastop2  36374  onsuct0  36454  weiunpo  36478  bj-bary1  37325  topdifinffinlem  37360  finorwe  37395  poimirlem24  37663  incsequz  37767  caushft  37780  equivbnd  37809  cntotbnd  37815  4atexlemex4  40091  frege124d  43773  gneispace  44146  expgrowth  44347  vk15.4j  44540  sstrALT2  44846  iccpartdisj  47447  fppr2odd  47741