Theorem syl6an 683

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  dfsb2  2493  xpcan  6176  xpcan2  6177  sucdom2OLD  9082  mapxpen  9143  sucdom2  9206  f1finf1oOLD  9272  unfiOLD  9313  inf3lem3  9625  dfac12r  10141  nnadju  10192  cfsuc  10252  fin23lem26  10320  iundom2g  10535  inar1  10770  rankcf  10772  ltsrpr  11072  supsrlem  11106  axpre-sup  11164  nominpos  12449  ublbneg  12917  qbtwnre  13178  fsequb  13940  fi1uzind  14458  brfi1indALT  14461  ccats1pfxeqrex  14665  rexanre  15293  rexuzre  15299  rexico  15300  caubnd  15305  rlim2lt  15441  rlim3  15442  lo1bddrp  15469  o1lo1  15481  climshftlem  15518  rlimcn3  15534  rlimo1  15561  lo1add  15571  lo1mul  15572  lo1le  15598  isercoll  15614  serf0  15627  cvgcmp  15762  dvds1lem  16211  dvds2lem  16212  mulmoddvds  16273  isprm5  16644  vdwlem2  16915  vdwlem10  16923  vdwlem11  16924  lsmcv  20754  lmconst  22765  ptcnplem  23125  fclscmp  23534  tsmsres  23648  addcnlem  24380  lebnumlem3  24479  xlebnum  24481  lebnumii  24482  iscmet3lem2  24809  bcthlem4  24844  cniccbdd  24978  ovoliunlem2  25020  mbfi1flimlem  25240  ply1divex  25654  aalioulem3  25847  aalioulem5  25849  aalioulem6  25850  aaliou  25851  ulmshftlem  25901  ulmbdd  25910  tanarg  26127  cxploglim  26482  ftalem2  26578  ftalem7  26583  dchrisumlem3  26994  frgrogt3nreg  29681  ubthlem3  30156  spansncol  30852  riesz1  31349  fineqvac  34128  erdsze2lem2  34226  dfrdg4  34954  neibastop2  35294  onsuct0  35374  bj-bary1  36241  topdifinffinlem  36276  finorwe  36311  poimirlem24  36560  incsequz  36664  caushft  36677  equivbnd  36706  cntotbnd  36712  4atexlemex4  38992  frege124d  42560  gneispace  42933  expgrowth  43142  vk15.4j  43337  sstrALT2  43644  iccpartdisj  46153  fppr2odd  46447