Theorem syl6an 690

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 413	. 2 ⊢ (𝜓 → (𝜃 → 𝜏))
5	1, 2, 4	sylsyld 61	1 ⊢ (𝜑 → (𝜒 → 𝜏))

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  dfsb2  2501  xpcan  6134  xpcan2  6135  mapxpen  9078  sucdom2  9134  inf3lem3  9549  dfac12r  10067  nnadju  10118  cfsuc  10177  fin23lem26  10245  iundom2g  10460  inar1  10696  rankcf  10698  ltsrpr  10998  supsrlem  11032  axpre-sup  11090  nominpos  12412  ublbneg  12881  qbtwnre  13149  fsequb  13935  fi1uzind  14467  brfi1indALT  14470  ccats1pfxeqrex  14675  rexanre  15307  rexuzre  15313  rexico  15314  caubnd  15319  rlim2lt  15457  rlim3  15458  lo1bddrp  15485  o1lo1  15497  climshftlem  15534  rlimcn3  15550  rlimo1  15577  lo1add  15587  lo1mul  15588  lo1le  15612  isercoll  15628  serf0  15641  cvgcmp  15777  dvds1lem  16234  dvds2lem  16235  mulmoddvds  16297  isprm5  16675  vdwlem2  16951  vdwlem10  16959  vdwlem11  16960  lsmcv  21141  lmconst  23251  ptcnplem  23611  fclscmp  24020  tsmsres  24134  addcnlem  24855  lebnumlem3  24955  xlebnum  24957  lebnumii  24958  iscmet3lem2  25284  bcthlem4  25319  cniccbdd  25453  ovoliunlem2  25495  mbfi1flimlem  25714  ply1divex  26127  aalioulem3  26325  aalioulem5  26327  aalioulem6  26328  aaliou  26329  ulmshftlem  26379  ulmbdd  26388  tanarg  26608  cxploglim  26966  ftalem2  27062  ftalem7  27067  dchrisumlem3  27479  frgrogt3nreg  30492  ubthlem3  30968  spansncol  31664  riesz1  32161  fineqvac  35307  erdsze2lem2  35433  dfrdg4  36180  neibastop2  36590  onsuct0  36670  weiunpo  36694  bj-bary1  37673  topdifinffinlem  37710  finorwe  37745  poimirlem24  38012  incsequz  38116  caushft  38129  equivbnd  38158  cntotbnd  38164  4atexlemex4  40566  frege124d  44206  gneispace  44579  expgrowth  44780  vk15.4j  44973  sstrALT2  45279  iccpartdisj  47913  fppr2odd  48223