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  6163  xpcan2  6164  mapxpen  9140  sucdom2  9196  inf3lem3  9609  dfac12r  10197  nnadju  10248  cfsuc  10307  fin23lem26  10375  iundom2g  10596  inar1  10832  rankcf  10834  ltsrpr  11134  supsrlem  11168  axpre-sup  11226  nominpos  12553  ublbneg  13030  qbtwnre  13299  fsequb  14087  fi1uzind  14620  brfi1indALT  14623  ccats1pfxeqrex  14832  rexanre  15482  rexuzre  15488  rexico  15489  caubnd  15494  rlim2lt  15632  rlim3  15633  lo1bddrp  15660  o1lo1  15672  climshftlem  15709  rlimcn3  15725  rlimo1  15752  lo1add  15762  lo1mul  15763  lo1le  15787  isercoll  15803  serf0  15816  cvgcmp  15951  dvds1lem  16405  dvds2lem  16406  mulmoddvds  16468  isprm5  16846  vdwlem2  17122  vdwlem10  17130  vdwlem11  17131  lsmcv  21381  lmconst  23541  ptcnplem  23902  fclscmp  24311  tsmsres  24425  addcnlem  25146  lebnumlem3  25246  xlebnum  25248  lebnumii  25249  iscmet3lem2  25575  bcthlem4  25610  cniccbdd  25744  ovoliunlem2  25786  mbfi1flimlem  26005  ply1divex  26417  aalioulem3  26625  aalioulem5  26627  aalioulem6  26628  aaliou  26629  ulmshftlem  26680  ulmbdd  26689  tanarg  26911  cxploglim  27269  ftalem2  27365  ftalem7  27370  dchrisumlem3  27782  frgrogt3nreg  30932  ubthlem3  31408  spansncol  32104  riesz1  32601  fineqvac  35709  erdsze2lem2  35890  dfrdg4  36637  neibastop2  37071  onsuct0  37151  weiunpo  37175  bj-bary1  38153  topdifinffinlem  38190  finorwe  38225  poimirlem24  38482  incsequz  38602  caushft  38615  equivbnd  38644  cntotbnd  38650  4atexlemex4  41050  frege124d  44705  gneispace  45078  expgrowth  45263  vk15.4j  45455  sstrALT2  45761  iccpartdisj  48441  fppr2odd  48751