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

This theorem is referenced by:  syl2an3an  1422  spc3egv  3616  euelss  4351  3elpr2eq  4930  funtpg  6633  fresaun  6792  fresaunres2  6793  ftpg  7190  eloprabga  7558  eloprabgaOLD  7559  elmapresaun  8938  djuenun  10240  addasspi  10964  mulasspi  10966  distrpi  10967  addcanpi  10968  mulcanpi  10969  ltapi  10972  lemul1  12146  ltdiv2  12181  zletr  12687  zdivadd  12714  eluzsub  12933  nn01to3  13006  qdivcl  13035  maxle  13253  lemin  13254  maxlt  13255  ltmin  13256  xaddass  13311  xmulasslem3  13348  xadddilem  13356  iooneg  13531  zltaddlt1le  13565  fzen  13601  fzaddel  13618  fzadd2  13619  fzrev  13647  fzrevral2  13670  fzshftral  13672  fzosubel2  13776  fzonn0p1p1  13795  fldiv2  13912  modmulnn  13940  modcyc2  13958  prsshashgt1  14459  hashssdif  14461  pfxccatin12lem4  14774  fsum0diag2  15831  binomrisefac  16090  efsub  16148  dvdsnegb  16322  muldvds1  16329  muldvds2  16330  dvdscmul  16331  dvdsmulc  16332  dvdscmulr  16333  dvdsmulcr  16334  dvds2add  16338  dvds2sub  16339  dvdstr  16342  addmodlteqALT  16373  divalglem8  16448  divalgb  16452  divalgmod  16454  ndvdsadd  16458  modgcd  16579  absmulgcd  16596  rpmulgcd  16604  zexpgcd  16612  cncongr2  16715  hashdvds  16822  pythagtriplem1  16863  vdwlem3  17030  ressinbas  17304  gsumws2  18877  mulgmodid  19153  nmzsubg  19205  pmtr3ncomlem1  19515  pmtrdifellem1  19518  subcmn  19879  gexexlem  19894  lsmcom  19900  zaddablx  19914  gsumpr  19997  c0snghm  20490  isdomn4  20738  drngmcl  20772  psgnghm  21621  phlssphl  21700  assa2ass  21906  psrbagconf1o  21972  gsumbagdiaglem  21973  psrass1lem  21975  psrass1  22007  mplmonmul  22077  psdmul  22193  ply1opprmul  22261  coe1mul  22294  2ndcdisj2  23486  fbssfi  23866  isfcf  24063  nmotri  24781  nghmplusg  24782  0nmhm  24797  iundisj2  25603  ovolioo  25622  uniiccdif  25632  basellem9  27150  cplgr2vpr  29468  redwlk  29708  clwwlknccat  30095  frgrwopreglem5a  30343  lnocoi  30789  ipasslem5  30867  hhssabloilem  31293  hhssnv  31296  shscli  31349  shmodsi  31421  lnopmi  32032  lnopcoi  32035  cnlnadjlem2  32100  adjmul  32124  leopmul2i  32167  leoptr  32169  pjimai  32208  mdslle1i  32349  mdslle2i  32350  mdslj1i  32351  mdslj2i  32352  mdslmd1lem1  32357  mdslmd2i  32362  atexch  32413  atcvatlem  32417  chirredlem3  32424  sumdmdii  32447  sumdmdlem  32450  cdj3i  32473  iundisj2f  32612  iundisj2fi  32802  xrge0omnd  33061  srafldlvec  33601  bnj1384  35008  revpfxsfxrev  35083  satffunlem2lem1  35372  cgr3permute3  36011  cgr3permute1  36012  cgr3com  36017  nndivsub  36423  lindsadd  37573  mblfinlem2  37618  cnambfre  37628  ftc1anclem5  37657  fzmul  37701  isismty  37761  heibor1  37770  heiborlem3  37773  hlatjcl  39323  hlatjcom  39324  hlatlej1  39331  hlrelat5N  39358  2lplnmN  39516  2llnmj  39517  2lplnmj  39579  factwoffsmonot  42199  syl3an12  42203  dvdsexpnn  42320  elmapresaunres2  42727  fzneg  42939  lsmfgcl  43031  trelded  44536  jaoded  44537  el123  44735  suctrALT  44797  suctrALTcf  44893  fnfocofob  46994  ltsubsubaddltsub  47216  fmtnoprmfac2lem1  47440  gboge9  47638  bgoldbtbndlem3  47681  usgrgrtrirex  47799  nnsgrp  47900  2zrngALT  47977  nn0sumltlt  48075  lincsum  48158  dignn0fr  48335  dignn0flhalflem2  48350