Theorem syl6an 685

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  dfsb2  2498  xpcan  6142  xpcan2  6143  mapxpen  9083  sucdom2  9139  inf3lem3  9551  dfac12r  10069  nnadju  10120  cfsuc  10179  fin23lem26  10247  iundom2g  10462  inar1  10698  rankcf  10700  ltsrpr  11000  supsrlem  11034  axpre-sup  11092  nominpos  12390  ublbneg  12858  qbtwnre  13126  fsequb  13910  fi1uzind  14442  brfi1indALT  14445  ccats1pfxeqrex  14650  rexanre  15282  rexuzre  15288  rexico  15289  caubnd  15294  rlim2lt  15432  rlim3  15433  lo1bddrp  15460  o1lo1  15472  climshftlem  15509  rlimcn3  15525  rlimo1  15552  lo1add  15562  lo1mul  15563  lo1le  15587  isercoll  15603  serf0  15616  cvgcmp  15751  dvds1lem  16206  dvds2lem  16207  mulmoddvds  16269  isprm5  16646  vdwlem2  16922  vdwlem10  16930  vdwlem11  16931  lsmcv  21108  lmconst  23217  ptcnplem  23577  fclscmp  23986  tsmsres  24100  addcnlem  24821  lebnumlem3  24930  xlebnum  24932  lebnumii  24933  iscmet3lem2  25260  bcthlem4  25295  cniccbdd  25430  ovoliunlem2  25472  mbfi1flimlem  25691  ply1divex  26110  aalioulem3  26310  aalioulem5  26312  aalioulem6  26313  aaliou  26314  ulmshftlem  26366  ulmbdd  26375  tanarg  26596  cxploglim  26956  ftalem2  27052  ftalem7  27057  dchrisumlem3  27470  frgrogt3nreg  30484  ubthlem3  30959  spansncol  31655  riesz1  32152  fineqvac  35291  erdsze2lem2  35417  dfrdg4  36164  neibastop2  36574  onsuct0  36654  weiunpo  36678  bj-bary1  37556  topdifinffinlem  37591  finorwe  37626  poimirlem24  37884  incsequz  37988  caushft  38001  equivbnd  38030  cntotbnd  38036  4atexlemex4  40438  frege124d  44106  gneispace  44479  expgrowth  44680  vk15.4j  44873  sstrALT2  45179  iccpartdisj  47786  fppr2odd  48080