Theorem syl6an 697

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  dfsb2  2522  xpcan  6167  xpcan2  6168  mapxpen  9163  sucdom2  9219  inf3lem3  9632  dfac12r  10226  nnadju  10277  cfsuc  10336  fin23lem26  10404  iundom2g  10625  inar1  10861  rankcf  10863  ltsrpr  11163  supsrlem  11197  axpre-sup  11255  nominpos  12584  ublbneg  13061  qbtwnre  13330  fsequb  14119  fi1uzind  14653  brfi1indALT  14656  ccats1pfxeqrex  14865  rexanre  15515  rexuzre  15521  rexico  15522  caubnd  15527  rlim2lt  15665  rlim3  15666  lo1bddrp  15693  o1lo1  15705  climshftlem  15742  rlimcn3  15758  rlimo1  15785  lo1add  15795  lo1mul  15796  lo1le  15820  isercoll  15836  serf0  15849  cvgcmp  15984  dvds1lem  16438  dvds2lem  16439  mulmoddvds  16501  isprm5  16884  vdwlem2  17161  vdwlem10  17169  vdwlem11  17170  lsmcv  21420  lmconst  23580  ptcnplem  23941  fclscmp  24350  tsmsres  24464  addcnlem  25185  lebnumlem3  25285  xlebnum  25287  lebnumii  25288  iscmet3lem2  25614  bcthlem4  25649  cniccbdd  25783  ovoliunlem2  25825  mbfi1flimlem  26044  ply1divex  26456  aalioulem3  26662  aalioulem5  26664  aalioulem6  26665  aaliou  26666  ulmshftlem  26717  ulmbdd  26726  tanarg  26948  cxploglim  27306  ftalem2  27402  ftalem7  27407  dchrisumlem3  27819  frgrogt3nreg  30999  ubthlem3  31475  spansncol  32171  riesz1  32668  acwer1prc  35809  fineqvac  35833  j0ltaleph  35940  erdsze2lem2  36038  dfrdg4  36790  neibastop2  37224  onsuct0  37304  weiunpo  37328  bj-bary1  38309  topdifinffinlem  38346  finorwe  38381  poimirlem24  38638  incsequz  38758  caushft  38771  equivbnd  38800  cntotbnd  38806  4atexlemex4  41206  frege124d  44837  gneispace  45210  expgrowth  45395  vk15.4j  45587  sstrALT2  45893  iccpartdisj  48595  fppr2odd  48905