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  2527  xpcan  6165  xpcan2  6166  mapxpen  9119  sucdom2  9175  inf3lem3  9587  dfac12r  10118  nnadju  10169  cfsuc  10229  fin23lem26  10297  iundom2g  10512  inar1  10748  rankcf  10750  ltsrpr  11050  supsrlem  11084  axpre-sup  11142  nominpos  12469  ublbneg  12945  qbtwnre  13213  fsequb  13999  fi1uzind  14532  brfi1indALT  14535  ccats1pfxeqrex  14740  rexanre  15386  rexuzre  15392  rexico  15393  caubnd  15398  rlim2lt  15536  rlim3  15537  lo1bddrp  15564  o1lo1  15576  climshftlem  15613  rlimcn3  15629  rlimo1  15656  lo1add  15666  lo1mul  15667  lo1le  15691  isercoll  15707  serf0  15720  cvgcmp  15856  dvds1lem  16313  dvds2lem  16314  mulmoddvds  16376  isprm5  16754  vdwlem2  17030  vdwlem10  17038  vdwlem11  17039  lsmcv  21231  lmconst  23375  ptcnplem  23735  fclscmp  24144  tsmsres  24258  addcnlem  24979  lebnumlem3  25079  xlebnum  25081  lebnumii  25082  iscmet3lem2  25408  bcthlem4  25443  cniccbdd  25577  ovoliunlem2  25619  mbfi1flimlem  25838  ply1divex  26251  aalioulem3  26452  aalioulem5  26454  aalioulem6  26455  aaliou  26456  ulmshftlem  26506  ulmbdd  26515  tanarg  26738  cxploglim  27096  ftalem2  27192  ftalem7  27197  dchrisumlem3  27609  frgrogt3nreg  30653  ubthlem3  31129  spansncol  31825  riesz1  32322  fineqvac  35419  erdsze2lem2  35562  dfrdg4  36309  neibastop2  36729  onsuct0  36809  weiunpo  36833  bj-bary1  37811  topdifinffinlem  37848  finorwe  37883  poimirlem24  38150  incsequz  38254  caushft  38267  equivbnd  38296  cntotbnd  38302  4atexlemex4  40704  frege124d  44344  gneispace  44717  expgrowth  44904  vk15.4j  45096  sstrALT2  45402  iccpartdisj  48042  fppr2odd  48352