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 1086

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  df-3an 1088

This theorem is referenced by:  syl2an3an  1424  spc3egv  3560  euelss  4285  3elpr2eq  4860  funtpg  6541  fresaun  6699  fresaunres2  6700  ftpg  7094  eloprabga  7462  elmapresaun  8814  djuenun  10084  addasspi  10808  mulasspi  10810  distrpi  10811  addcanpi  10812  mulcanpi  10813  ltapi  10816  lemul1  11994  ltdiv2  12029  zletr  12537  zdivadd  12565  eluzsub  12783  nn01to3  12860  qdivcl  12889  maxle  13111  lemin  13112  maxlt  13113  ltmin  13114  xaddass  13169  xmulasslem3  13206  xadddilem  13214  iooneg  13392  zltaddlt1le  13426  fzen  13462  fzaddel  13479  fzadd2  13480  fzrev  13508  fzrevral2  13534  fzshftral  13536  fzosubel2  13646  fzonn0p1p1  13665  fldiv2  13783  modmulnn  13811  modcyc2  13829  prsshashgt1  14335  hashssdif  14337  pfxccatin12lem4  14650  fsum0diag2  15708  binomrisefac  15967  efsub  16027  dvdsnegb  16202  muldvds1  16209  muldvds2  16210  dvdscmul  16211  dvdsmulc  16212  dvdscmulr  16213  dvdsmulcr  16214  dvds2add  16219  dvds2sub  16220  dvdstr  16223  addmodlteqALT  16254  divalglem8  16329  divalgb  16333  divalgmod  16335  ndvdsadd  16339  modgcd  16461  absmulgcd  16478  rpmulgcd  16486  zexpgcd  16494  cncongr2  16597  hashdvds  16704  pythagtriplem1  16746  vdwlem3  16913  ressinbas  17174  gsumws2  18734  mulgmodid  19010  nmzsubg  19062  pmtr3ncomlem1  19370  pmtrdifellem1  19373  subcmn  19734  gexexlem  19749  lsmcom  19755  zaddablx  19769  gsumpr  19852  c0snghm  20367  isdomn4  20619  drngmcl  20653  xrge0omnd  21370  psgnghm  21505  phlssphl  21584  assa2ass  21788  psrbagconf1o  21854  gsumbagdiaglem  21855  psrass1lem  21857  psrass1  21889  mplmonmul  21959  psdmul  22069  ply1opprmul  22139  coe1mul  22172  2ndcdisj2  23360  fbssfi  23740  isfcf  23937  nmotri  24643  nghmplusg  24644  0nmhm  24659  iundisj2  25466  ovolioo  25485  uniiccdif  25495  basellem9  27015  zsoring  28319  cplgr2vpr  29396  redwlk  29634  clwwlknccat  30025  frgrwopreglem5a  30273  lnocoi  30719  ipasslem5  30797  hhssabloilem  31223  hhssnv  31226  shscli  31279  shmodsi  31351  lnopmi  31962  lnopcoi  31965  cnlnadjlem2  32030  adjmul  32054  leopmul2i  32097  leoptr  32099  pjimai  32138  mdslle1i  32279  mdslle2i  32280  mdslj1i  32281  mdslj2i  32282  mdslmd1lem1  32287  mdslmd2i  32292  atexch  32343  atcvatlem  32347  chirredlem3  32354  sumdmdii  32377  sumdmdlem  32380  cdj3i  32403  iundisj2f  32552  iundisj2fi  32753  srafldlvec  33558  bnj1384  34998  revpfxsfxrev  35088  satffunlem2lem1  35376  cgr3permute3  36020  cgr3permute1  36021  cgr3com  36026  nndivsub  36430  lindsadd  37592  mblfinlem2  37637  cnambfre  37647  ftc1anclem5  37676  fzmul  37720  isismty  37780  heibor1  37789  heiborlem3  37792  hlatjcl  39345  hlatjcom  39346  hlatlej1  39353  hlrelat5N  39380  2lplnmN  39538  2llnmj  39539  2lplnmj  39601  syl3an12  42182  dvdsexpnn  42306  elmapresaunres2  42744  fzneg  42955  lsmfgcl  43047  trelded  44539  jaoded  44540  el123  44737  suctrALT  44799  suctrALTcf  44895  fnfocofob  47064  ltsubsubaddltsub  47286  fmtnoprmfac2lem1  47551  gboge9  47749  bgoldbtbndlem3  47792  usgrgrtrirex  47935  gpgedg2iv  48052  nnsgrp  48162  2zrngALT  48239  nn0sumltlt  48335  lincsum  48415  dignn0fr  48587  dignn0flhalflem2  48602