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  2524  xpcan  6173  xpcan2  6174  mapxpen  9144  sucdom2  9200  inf3lem3  9612  dfac12r  10152  nnadju  10203  cfsuc  10262  fin23lem26  10330  iundom2g  10551  inar1  10787  rankcf  10789  ltsrpr  11089  supsrlem  11123  axpre-sup  11181  nominpos  12508  ublbneg  12985  qbtwnre  13253  fsequb  14041  fi1uzind  14574  brfi1indALT  14577  ccats1pfxeqrex  14786  rexanre  15436  rexuzre  15442  rexico  15443  caubnd  15448  rlim2lt  15586  rlim3  15587  lo1bddrp  15614  o1lo1  15626  climshftlem  15663  rlimcn3  15679  rlimo1  15706  lo1add  15716  lo1mul  15717  lo1le  15741  isercoll  15757  serf0  15770  cvgcmp  15905  dvds1lem  16361  dvds2lem  16362  mulmoddvds  16424  isprm5  16802  vdwlem2  17078  vdwlem10  17086  vdwlem11  17087  lsmcv  21332  lmconst  23490  ptcnplem  23851  fclscmp  24260  tsmsres  24374  addcnlem  25095  lebnumlem3  25195  xlebnum  25197  lebnumii  25198  iscmet3lem2  25524  bcthlem4  25559  cniccbdd  25693  ovoliunlem2  25735  mbfi1flimlem  25954  ply1divex  26367  aalioulem3  26570  aalioulem5  26572  aalioulem6  26573  aaliou  26574  ulmshftlem  26625  ulmbdd  26634  tanarg  26857  cxploglim  27215  ftalem2  27311  ftalem7  27316  dchrisumlem3  27728  frgrogt3nreg  30878  ubthlem3  31354  spansncol  32050  riesz1  32547  fineqvac  35644  erdsze2lem2  35785  dfrdg4  36532  neibastop2  36982  onsuct0  37062  weiunpo  37086  bj-bary1  38066  topdifinffinlem  38103  finorwe  38138  poimirlem24  38395  incsequz  38500  caushft  38513  equivbnd  38542  cntotbnd  38548  4atexlemex4  40948  frege124d  44603  gneispace  44976  expgrowth  45161  vk15.4j  45353  sstrALT2  45659  iccpartdisj  48339  fppr2odd  48649