Theorem syl6an 684

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  dfsb2  2491  xpcan  6129  xpcan2  6130  mapxpen  9067  sucdom2  9127  f1finf1oOLD  9175  inf3lem3  9545  dfac12r  10060  nnadju  10111  cfsuc  10170  fin23lem26  10238  iundom2g  10453  inar1  10688  rankcf  10690  ltsrpr  10990  supsrlem  11024  axpre-sup  11082  nominpos  12379  ublbneg  12852  qbtwnre  13119  fsequb  13900  fi1uzind  14432  brfi1indALT  14435  ccats1pfxeqrex  14639  rexanre  15272  rexuzre  15278  rexico  15279  caubnd  15284  rlim2lt  15422  rlim3  15423  lo1bddrp  15450  o1lo1  15462  climshftlem  15499  rlimcn3  15515  rlimo1  15542  lo1add  15552  lo1mul  15553  lo1le  15577  isercoll  15593  serf0  15606  cvgcmp  15741  dvds1lem  16196  dvds2lem  16197  mulmoddvds  16259  isprm5  16636  vdwlem2  16912  vdwlem10  16920  vdwlem11  16921  lsmcv  21066  lmconst  23164  ptcnplem  23524  fclscmp  23933  tsmsres  24047  addcnlem  24769  lebnumlem3  24878  xlebnum  24880  lebnumii  24881  iscmet3lem2  25208  bcthlem4  25243  cniccbdd  25378  ovoliunlem2  25420  mbfi1flimlem  25639  ply1divex  26058  aalioulem3  26258  aalioulem5  26260  aalioulem6  26261  aaliou  26262  ulmshftlem  26314  ulmbdd  26323  tanarg  26544  cxploglim  26904  ftalem2  27000  ftalem7  27005  dchrisumlem3  27418  frgrogt3nreg  30359  ubthlem3  30834  spansncol  31530  riesz1  32027  fineqvac  35071  erdsze2lem2  35176  dfrdg4  35924  neibastop2  36334  onsuct0  36414  weiunpo  36438  bj-bary1  37285  topdifinffinlem  37320  finorwe  37355  poimirlem24  37623  incsequz  37727  caushft  37740  equivbnd  37769  cntotbnd  37775  4atexlemex4  40052  frege124d  43734  gneispace  44107  expgrowth  44308  vk15.4j  44502  sstrALT2  44808  iccpartdisj  47422  fppr2odd  47716