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 ⊢ (𝜑 → (𝜒 → 𝜏))

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

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 401

This theorem is used by:  dfsb2  2524  xpcan  6173  xpcan2  6174  mapxpen  9129  sucdom2  9185  inf3lem3  9597  dfac12r  10137  nnadju  10188  cfsuc  10247  fin23lem26  10315  iundom2g  10530  inar1  10766  rankcf  10768  ltsrpr  11068  supsrlem  11102  axpre-sup  11160  nominpos  12487  ublbneg  12963  qbtwnre  13231  fsequb  14018  fi1uzind  14551  brfi1indALT  14554  ccats1pfxeqrex  14759  rexanre  15405  rexuzre  15411  rexico  15412  caubnd  15417  rlim2lt  15555  rlim3  15556  lo1bddrp  15583  o1lo1  15595  climshftlem  15632  rlimcn3  15648  rlimo1  15675  lo1add  15685  lo1mul  15686  lo1le  15710  isercoll  15726  serf0  15739  cvgcmp  15875  dvds1lem  16331  dvds2lem  16332  mulmoddvds  16394  isprm5  16772  vdwlem2  17048  vdwlem10  17056  vdwlem11  17057  lsmcv  21276  lmconst  23429  ptcnplem  23789  fclscmp  24198  tsmsres  24312  addcnlem  25033  lebnumlem3  25133  xlebnum  25135  lebnumii  25136  iscmet3lem2  25462  bcthlem4  25497  cniccbdd  25631  ovoliunlem2  25673  mbfi1flimlem  25892  ply1divex  26305  aalioulem3  26508  aalioulem5  26510  aalioulem6  26511  aaliou  26512  ulmshftlem  26563  ulmbdd  26572  tanarg  26795  cxploglim  27153  ftalem2  27249  ftalem7  27254  dchrisumlem3  27666  frgrogt3nreg  30759  ubthlem3  31235  spansncol  31931  riesz1  32428  fineqvac  35537  erdsze2lem2  35704  dfrdg4  36451  neibastop2  36900  onsuct0  36980  weiunpo  37004  bj-bary1  37984  topdifinffinlem  38021  finorwe  38056  poimirlem24  38323  incsequz  38427  caushft  38440  equivbnd  38469  cntotbnd  38475  4atexlemex4  40875  frege124d  44515  gneispace  44888  expgrowth  45073  vk15.4j  45265  sstrALT2  45571  iccpartdisj  48214  fppr2odd  48524