Theorem syl6an 696

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  dfsb2  2523  xpcan  6174  xpcan2  6175  mapxpen  9130  sucdom2  9186  inf3lem3  9598  dfac12r  10129  nnadju  10180  cfsuc  10240  fin23lem26  10308  iundom2g  10523  inar1  10759  rankcf  10761  ltsrpr  11061  supsrlem  11095  axpre-sup  11153  nominpos  12480  ublbneg  12956  qbtwnre  13224  fsequb  14011  fi1uzind  14544  brfi1indALT  14547  ccats1pfxeqrex  14752  rexanre  15398  rexuzre  15404  rexico  15405  caubnd  15410  rlim2lt  15548  rlim3  15549  lo1bddrp  15576  o1lo1  15588  climshftlem  15625  rlimcn3  15641  rlimo1  15668  lo1add  15678  lo1mul  15679  lo1le  15703  isercoll  15719  serf0  15732  cvgcmp  15868  dvds1lem  16324  dvds2lem  16325  mulmoddvds  16387  isprm5  16765  vdwlem2  17041  vdwlem10  17049  vdwlem11  17050  lsmcv  21244  lmconst  23397  ptcnplem  23757  fclscmp  24166  tsmsres  24280  addcnlem  25001  lebnumlem3  25101  xlebnum  25103  lebnumii  25104  iscmet3lem2  25430  bcthlem4  25465  cniccbdd  25599  ovoliunlem2  25641  mbfi1flimlem  25860  ply1divex  26273  aalioulem3  26474  aalioulem5  26476  aalioulem6  26477  aaliou  26478  ulmshftlem  26528  ulmbdd  26537  tanarg  26760  cxploglim  27118  ftalem2  27214  ftalem7  27219  dchrisumlem3  27631  frgrogt3nreg  30714  ubthlem3  31190  spansncol  31886  riesz1  32383  fineqvac  35495  erdsze2lem2  35662  dfrdg4  36409  neibastop2  36838  onsuct0  36918  weiunpo  36942  bj-bary1  37922  topdifinffinlem  37959  finorwe  37994  poimirlem24  38261  incsequz  38365  caushft  38378  equivbnd  38407  cntotbnd  38413  4atexlemex4  40815  frege124d  44457  gneispace  44830  expgrowth  45015  vk15.4j  45207  sstrALT2  45513  iccpartdisj  48153  fppr2odd  48463