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  6171  xpcan2  6172  sucdom2OLD  9077  mapxpen  9138  sucdom2  9201  f1finf1oOLD  9267  unfiOLD  9308  inf3lem3  9620  dfac12r  10136  nnadju  10187  cfsuc  10247  fin23lem26  10315  iundom2g  10530  inar1  10765  rankcf  10767  ltsrpr  11067  supsrlem  11101  axpre-sup  11159  nominpos  12444  ublbneg  12912  qbtwnre  13173  fsequb  13935  fi1uzind  14453  brfi1indALT  14456  ccats1pfxeqrex  14660  rexanre  15288  rexuzre  15294  rexico  15295  caubnd  15300  rlim2lt  15436  rlim3  15437  lo1bddrp  15464  o1lo1  15476  climshftlem  15513  rlimcn3  15529  rlimo1  15556  lo1add  15566  lo1mul  15567  lo1le  15593  isercoll  15609  serf0  15622  cvgcmp  15757  dvds1lem  16206  dvds2lem  16207  mulmoddvds  16268  isprm5  16639  vdwlem2  16910  vdwlem10  16918  vdwlem11  16919  lsmcv  20741  lmconst  22746  ptcnplem  23106  fclscmp  23515  tsmsres  23629  addcnlem  24361  lebnumlem3  24460  xlebnum  24462  lebnumii  24463  iscmet3lem2  24790  bcthlem4  24825  cniccbdd  24959  ovoliunlem2  25001  mbfi1flimlem  25221  ply1divex  25635  aalioulem3  25828  aalioulem5  25830  aalioulem6  25831  aaliou  25832  ulmshftlem  25882  ulmbdd  25891  tanarg  26108  cxploglim  26461  ftalem2  26557  ftalem7  26562  dchrisumlem3  26973  frgrogt3nreg  29629  ubthlem3  30102  spansncol  30798  riesz1  31295  fineqvac  34034  erdsze2lem2  34132  dfrdg4  34860  neibastop2  35183  onsuct0  35263  bj-bary1  36130  topdifinffinlem  36165  finorwe  36200  poimirlem24  36449  incsequz  36553  caushft  36566  equivbnd  36595  cntotbnd  36601  4atexlemex4  38881  frege124d  42444  gneispace  42817  expgrowth  43026  vk15.4j  43221  sstrALT2  43528  iccpartdisj  46039  fppr2odd  46333