Theorem syl6an 680

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 206  df-an 396

This theorem is referenced by:  dfsb2  2497  xpcan  6068  xpcan2  6069  sucdom2  8822  mapxpen  8879  f1finf1o  8975  unfiOLD  9011  inf3lem3  9318  dfac12r  9833  nnadju  9884  cfsuc  9944  fin23lem26  10012  iundom2g  10227  inar1  10462  rankcf  10464  ltsrpr  10764  supsrlem  10798  axpre-sup  10856  nominpos  12140  ublbneg  12602  qbtwnre  12862  fsequb  13623  fi1uzind  14139  brfi1indALT  14142  ccats1pfxeqrex  14356  rexanre  14986  rexuzre  14992  rexico  14993  caubnd  14998  rlim2lt  15134  rlim3  15135  lo1bddrp  15162  o1lo1  15174  climshftlem  15211  rlimcn3  15227  rlimo1  15254  lo1add  15264  lo1mul  15265  lo1le  15291  isercoll  15307  serf0  15320  cvgcmp  15456  dvds1lem  15905  dvds2lem  15906  mulmoddvds  15967  isprm5  16340  vdwlem2  16611  vdwlem10  16619  vdwlem11  16620  lsmcv  20318  lmconst  22320  ptcnplem  22680  fclscmp  23089  tsmsres  23203  addcnlem  23933  lebnumlem3  24032  xlebnum  24034  lebnumii  24035  iscmet3lem2  24361  bcthlem4  24396  cniccbdd  24530  ovoliunlem2  24572  mbfi1flimlem  24792  ply1divex  25206  aalioulem3  25399  aalioulem5  25401  aalioulem6  25402  aaliou  25403  ulmshftlem  25453  ulmbdd  25462  tanarg  25679  cxploglim  26032  ftalem2  26128  ftalem7  26133  dchrisumlem3  26544  frgrogt3nreg  28662  ubthlem3  29135  spansncol  29831  riesz1  30328  fineqvac  32966  erdsze2lem2  33066  dfrdg4  34180  neibastop2  34477  onsuct0  34557  bj-bary1  35410  topdifinffinlem  35445  finorwe  35480  poimirlem24  35728  incsequz  35833  caushft  35846  equivbnd  35875  cntotbnd  35881  4atexlemex4  38014  frege124d  41258  gneispace  41633  expgrowth  41842  vk15.4j  42037  sstrALT2  42344  iccpartdisj  44777  fppr2odd  45071