Theorem syl3an 1157

Description: A triple syllogism inference. (Contributed by NM, 13-May-2004.)

Hypotheses

Ref	Expression
syl3an.1	⊢ (𝜑 → 𝜓)
syl3an.2	⊢ (𝜒 → 𝜃)
syl3an.3	⊢ (𝜏 → 𝜂)
syl3an.4	⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)

Assertion

Ref	Expression
syl3an	⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)

Proof of Theorem syl3an

Step	Hyp	Ref	Expression
1		syl3an.1	. . 3 ⊢ (𝜑 → 𝜓)
2		syl3an.2	. . 3 ⊢ (𝜒 → 𝜃)
3		syl3an.3	. . 3 ⊢ (𝜏 → 𝜂)
4	1, 2, 3	3anim123i 1148	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))
5		syl3an.4	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)
6	4, 5	syl 17	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  syl2an3an  1419  spc3egv  3589  euelss  4324  3elpr2eq  4912  funtpg  6614  fresaun  6773  fresaunres2  6774  ftpg  7170  eloprabga  7533  eloprabgaOLD  7534  elmapresaun  8909  djuenun  10213  addasspi  10938  mulasspi  10940  distrpi  10941  addcanpi  10942  mulcanpi  10943  ltapi  10946  lemul1  12117  ltdiv2  12152  zletr  12658  zdivadd  12685  eluzsub  12904  nn01to3  12977  qdivcl  13006  maxle  13224  lemin  13225  maxlt  13226  ltmin  13227  xaddass  13282  xmulasslem3  13319  xadddilem  13327  iooneg  13502  zltaddlt1le  13536  fzen  13572  fzaddel  13589  fzadd2  13590  fzrev  13618  fzrevral2  13641  fzshftral  13643  fzosubel2  13746  fzonn0p1p1  13765  fldiv2  13881  modmulnn  13909  modcyc2  13927  prsshashgt1  14427  hashssdif  14429  pfxccatin12lem4  14734  fsum0diag2  15787  binomrisefac  16044  efsub  16102  dvdsnegb  16276  muldvds1  16283  muldvds2  16284  dvdscmul  16285  dvdsmulc  16286  dvdscmulr  16287  dvdsmulcr  16288  dvds2add  16292  dvds2sub  16293  dvdstr  16296  addmodlteqALT  16327  divalglem8  16402  divalgb  16406  divalgmod  16408  ndvdsadd  16412  modgcd  16533  absmulgcd  16550  rpmulgcd  16558  zexpgcd  16566  cncongr2  16669  hashdvds  16777  pythagtriplem1  16818  vdwlem3  16985  ressinbas  17259  gsumws2  18832  mulgmodid  19107  nmzsubg  19159  pmtr3ncomlem1  19471  pmtrdifellem1  19474  subcmn  19835  gexexlem  19850  lsmcom  19856  zaddablx  19870  gsumpr  19953  c0snghm  20446  isdomn4  20694  drngmcl  20728  psgnghm  21576  phlssphl  21655  assa2ass  21861  psrbagconf1o  21934  psrbagconf1oOLD  21935  gsumbagdiaglemOLD  21936  psrass1lemOLD  21938  gsumbagdiaglem  21939  psrass1lem  21941  psrass1  21973  mplmonmul  22043  psdmul  22160  ply1opprmul  22228  coe1mul  22261  2ndcdisj2  23452  fbssfi  23832  isfcf  24029  nmotri  24747  nghmplusg  24748  0nmhm  24763  iundisj2  25569  ovolioo  25588  uniiccdif  25598  basellem9  27117  cplgr2vpr  29369  redwlk  29609  clwwlknccat  29996  frgrwopreglem5a  30244  lnocoi  30690  ipasslem5  30768  hhssabloilem  31194  hhssnv  31197  shscli  31250  shmodsi  31322  lnopmi  31933  lnopcoi  31936  cnlnadjlem2  32001  adjmul  32025  leopmul2i  32068  leoptr  32070  pjimai  32109  mdslle1i  32250  mdslle2i  32251  mdslj1i  32252  mdslj2i  32253  mdslmd1lem1  32258  mdslmd2i  32263  atexch  32314  atcvatlem  32318  chirredlem3  32325  sumdmdii  32348  sumdmdlem  32351  cdj3i  32374  iundisj2f  32510  iundisj2fi  32699  xrge0omnd  32946  srafldlvec  33483  bnj1384  34877  revpfxsfxrev  34943  satffunlem2lem1  35232  cgr3permute3  35871  cgr3permute1  35872  cgr3com  35877  nndivsub  36169  lindsadd  37314  mblfinlem2  37359  cnambfre  37369  ftc1anclem5  37398  fzmul  37442  isismty  37502  heibor1  37511  heiborlem3  37514  hlatjcl  39065  hlatjcom  39066  hlatlej1  39073  hlrelat5N  39100  2lplnmN  39258  2llnmj  39259  2lplnmj  39321  factwoffsmonot  41928  syl3an12  41932  dvdsexpnn  42128  elmapresaunres2  42428  fzneg  42640  lsmfgcl  42735  trelded  44241  jaoded  44242  el123  44440  suctrALT  44502  suctrALTcf  44598  fnfocofob  46692  ltsubsubaddltsub  46914  fmtnoprmfac2lem1  47138  gboge9  47336  bgoldbtbndlem3  47379  nnsgrp  47554  2zrngALT  47631  nn0sumltlt  47729  lincsum  47812  dignn0fr  47989  dignn0flhalflem2  48004