Theorem syl6an 692

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  dfsb2  2518  xpcan  6151  xpcan2  6152  mapxpen  9104  sucdom2  9160  inf3lem3  9575  dfac12r  10093  nnadju  10144  cfsuc  10204  fin23lem26  10272  iundom2g  10487  inar1  10723  rankcf  10725  ltsrpr  11025  supsrlem  11059  axpre-sup  11117  nominpos  12448  ublbneg  12924  qbtwnre  13192  fsequb  13978  fi1uzind  14510  brfi1indALT  14513  ccats1pfxeqrex  14718  rexanre  15350  rexuzre  15356  rexico  15357  caubnd  15362  rlim2lt  15500  rlim3  15501  lo1bddrp  15528  o1lo1  15540  climshftlem  15577  rlimcn3  15593  rlimo1  15620  lo1add  15630  lo1mul  15631  lo1le  15655  isercoll  15671  serf0  15684  cvgcmp  15820  dvds1lem  16277  dvds2lem  16278  mulmoddvds  16340  isprm5  16718  vdwlem2  16994  vdwlem10  17002  vdwlem11  17003  lsmcv  21184  lmconst  23294  ptcnplem  23654  fclscmp  24063  tsmsres  24177  addcnlem  24898  lebnumlem3  24998  xlebnum  25000  lebnumii  25001  iscmet3lem2  25327  bcthlem4  25362  cniccbdd  25496  ovoliunlem2  25538  mbfi1flimlem  25757  ply1divex  26170  aalioulem3  26368  aalioulem5  26370  aalioulem6  26371  aaliou  26372  ulmshftlem  26422  ulmbdd  26431  tanarg  26654  cxploglim  27012  ftalem2  27108  ftalem7  27113  dchrisumlem3  27525  frgrogt3nreg  30538  ubthlem3  31014  spansncol  31710  riesz1  32207  fineqvac  35367  erdsze2lem2  35502  dfrdg4  36249  neibastop2  36669  onsuct0  36749  weiunpo  36773  bj-bary1  37752  topdifinffinlem  37789  finorwe  37824  poimirlem24  38091  incsequz  38195  caushft  38208  equivbnd  38237  cntotbnd  38243  4atexlemex4  40645  frege124d  44285  gneispace  44658  expgrowth  44859  vk15.4j  45052  sstrALT2  45358  iccpartdisj  47991  fppr2odd  48301