Theorem syl3an 1160

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 1151	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))
5		syl3an.4	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)
6	4, 5	syl 17	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  syl2an3an  1422  spc3egv  3593  euelss  4321  3elpr2eq  4907  funtpg  6603  fresaun  6762  fresaunres2  6763  ftpg  7156  eloprabga  7518  eloprabgaOLD  7519  elmapresaun  8876  djuenun  10167  addasspi  10892  mulasspi  10894  distrpi  10895  addcanpi  10896  mulcanpi  10897  ltapi  10900  lemul1  12070  ltdiv2  12104  zletr  12610  zdivadd  12637  eluzsub  12856  nn01to3  12929  qdivcl  12958  maxle  13174  lemin  13175  maxlt  13176  ltmin  13177  xaddass  13232  xmulasslem3  13269  xadddilem  13277  iooneg  13452  zltaddlt1le  13486  fzen  13522  fzaddel  13539  fzadd2  13540  fzrev  13568  fzrevral2  13591  fzshftral  13593  fzosubel2  13696  fzonn0p1p1  13715  fldiv2  13830  modmulnn  13858  modcyc2  13876  prsshashgt1  14374  hashssdif  14376  pfxccatin12lem4  14680  fsum0diag2  15733  binomrisefac  15990  efsub  16047  dvdsnegb  16221  muldvds1  16228  muldvds2  16229  dvdscmul  16230  dvdsmulc  16231  dvdscmulr  16232  dvdsmulcr  16233  dvds2add  16237  dvds2sub  16238  dvdstr  16241  addmodlteqALT  16272  divalglem8  16347  divalgb  16351  divalgmod  16353  ndvdsadd  16357  modgcd  16478  absmulgcd  16495  rpmulgcd  16502  cncongr2  16609  hashdvds  16712  pythagtriplem1  16753  vdwlem3  16920  ressinbas  17194  gsumws2  18759  mulgmodid  19029  nmzsubg  19081  pmtr3ncomlem1  19382  pmtrdifellem1  19385  subcmn  19746  gexexlem  19761  lsmcom  19767  zaddablx  19781  gsumpr  19864  c0snghm  20355  isdomn4  21118  psgnghm  21352  phlssphl  21431  assa2ass  21637  psrbagconf1o  21708  psrbagconf1oOLD  21709  gsumbagdiaglemOLD  21710  psrass1lemOLD  21712  gsumbagdiaglem  21713  psrass1lem  21715  psrass1  21744  mplmonmul  21810  ply1opprmul  21981  coe1mul  22012  2ndcdisj2  23181  fbssfi  23561  isfcf  23758  nmotri  24476  nghmplusg  24477  0nmhm  24492  iundisj2  25290  ovolioo  25309  uniiccdif  25319  basellem9  26817  cplgr2vpr  28945  redwlk  29184  clwwlknccat  29571  frgrwopreglem5a  29819  lnocoi  30265  ipasslem5  30343  hhssabloilem  30769  hhssnv  30772  shscli  30825  shmodsi  30897  lnopmi  31508  lnopcoi  31511  cnlnadjlem2  31576  adjmul  31600  leopmul2i  31643  leoptr  31645  pjimai  31684  mdslle1i  31825  mdslle2i  31826  mdslj1i  31827  mdslj2i  31828  mdslmd1lem1  31833  mdslmd2i  31838  atexch  31889  atcvatlem  31893  chirredlem3  31900  sumdmdii  31923  sumdmdlem  31926  cdj3i  31949  iundisj2f  32076  iundisj2fi  32263  xrge0omnd  32487  srafldlvec  32949  bnj1384  34329  revpfxsfxrev  34392  satffunlem2lem1  34681  cgr3permute3  35311  cgr3permute1  35312  cgr3com  35317  nndivsub  35645  lindsadd  36784  mblfinlem2  36829  cnambfre  36839  ftc1anclem5  36868  fzmul  36912  isismty  36972  heibor1  36981  heiborlem3  36984  hlatjcl  38540  hlatjcom  38541  hlatlej1  38548  hlrelat5N  38575  2lplnmN  38733  2llnmj  38734  2lplnmj  38796  factwoffsmonot  41329  syl3an12  41332  zexpgcd  41529  dvdsexpnn  41533  elmapresaunres2  41811  fzneg  42023  lsmfgcl  42118  trelded  43628  jaoded  43629  el123  43827  suctrALT  43889  suctrALTcf  43985  fnfocofob  46086  ltsubsubaddltsub  46308  fmtnoprmfac2lem1  46533  gboge9  46731  bgoldbtbndlem3  46774  nnsgrp  46854  2zrngALT  46935  nn0sumltlt  47115  lincsum  47198  dignn0fr  47375  dignn0flhalflem2  47390