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  29650  ubthlem3  30125  spansncol  30821  riesz1  31318  fineqvac  34097  erdsze2lem2  34195  dfrdg4  34923  neibastop2  35246  onsuct0  35326  bj-bary1  36193  topdifinffinlem  36228  finorwe  36263  poimirlem24  36512  incsequz  36616  caushft  36629  equivbnd  36658  cntotbnd  36664  4atexlemex4  38944  frege124d  42512  gneispace  42885  expgrowth  43094  vk15.4j  43289  sstrALT2  43596  iccpartdisj  46105  fppr2odd  46399