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  6166  xpcan2  6167  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  12472  ublbneg  12948  qbtwnre  13216  fsequb  14002  fi1uzind  14534  brfi1indALT  14537  ccats1pfxeqrex  14742  rexanre  15388  rexuzre  15394  rexico  15395  caubnd  15400  rlim2lt  15538  rlim3  15539  lo1bddrp  15566  o1lo1  15578  climshftlem  15615  rlimcn3  15631  rlimo1  15658  lo1add  15668  lo1mul  15669  lo1le  15693  isercoll  15709  serf0  15722  cvgcmp  15858  dvds1lem  16315  dvds2lem  16316  mulmoddvds  16378  isprm5  16756  vdwlem2  17032  vdwlem10  17040  vdwlem11  17041  lsmcv  21234  lmconst  23379  ptcnplem  23739  fclscmp  24148  tsmsres  24262  addcnlem  24983  lebnumlem3  25083  xlebnum  25085  lebnumii  25086  iscmet3lem2  25412  bcthlem4  25447  cniccbdd  25581  ovoliunlem2  25623  mbfi1flimlem  25842  ply1divex  26255  aalioulem3  26456  aalioulem5  26458  aalioulem6  26459  aaliou  26460  ulmshftlem  26510  ulmbdd  26519  tanarg  26742  cxploglim  27100  ftalem2  27196  ftalem7  27201  dchrisumlem3  27613  frgrogt3nreg  30657  ubthlem3  31133  spansncol  31829  riesz1  32326  fineqvac  35424  erdsze2lem2  35567  dfrdg4  36314  neibastop2  36734  onsuct0  36814  weiunpo  36838  bj-bary1  37816  topdifinffinlem  37853  finorwe  37888  poimirlem24  38155  incsequz  38259  caushft  38272  equivbnd  38301  cntotbnd  38307  4atexlemex4  40709  frege124d  44349  gneispace  44722  expgrowth  44909  vk15.4j  45102  sstrALT2  45408  iccpartdisj  48041  fppr2odd  48351