Theorem syl3an 1162

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

Syntax hints:   → wi 4   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  syl2an3an  1424  spc3egv  3518  euelss  4236  3elpr2eq  4818  funtpg  6435  fresaun  6590  fresaunres2  6591  ftpg  6971  eloprabga  7318  eloprabgaOLD  7319  elmapresaun  8561  djuenun  9784  addasspi  10509  mulasspi  10511  distrpi  10512  addcanpi  10513  mulcanpi  10514  ltapi  10517  lemul1  11684  ltdiv2  11718  zletr  12221  zdivadd  12248  nn01to3  12537  qdivcl  12566  maxle  12781  lemin  12782  maxlt  12783  ltmin  12784  xaddass  12839  xmulasslem3  12876  xadddilem  12884  iooneg  13059  zltaddlt1le  13093  fzen  13129  fzaddel  13146  fzadd2  13147  fzrev  13175  fzrevral2  13198  fzshftral  13200  fzosubel2  13302  fzonn0p1p1  13321  fldiv2  13434  modmulnn  13462  modcyc2  13480  prsshashgt1  13977  hashssdif  13979  ccatw2s1assOLD  14193  pfxccatin12lem4  14291  fsum0diag2  15347  binomrisefac  15604  efsub  15661  dvdsnegb  15835  muldvds1  15842  muldvds2  15843  dvdscmul  15844  dvdsmulc  15845  dvdscmulr  15846  dvdsmulcr  15847  dvds2add  15851  dvds2sub  15852  dvdstr  15855  addmodlteqALT  15886  divalglem8  15961  divalgb  15965  divalgmod  15967  ndvdsadd  15971  modgcd  16092  absmulgcd  16109  rpmulgcd  16118  cncongr2  16225  hashdvds  16328  pythagtriplem1  16369  vdwlem3  16536  ressinbas  16797  gsumws2  18269  mulgmodid  18530  nmzsubg  18581  pmtr3ncomlem1  18865  pmtrdifellem1  18868  subcmn  19222  gexexlem  19237  lsmcom  19243  zaddablx  19257  gsumpr  19340  psgnghm  20542  phlssphl  20621  assa2ass  20825  psrbagconf1o  20895  psrbagconf1oOLD  20896  gsumbagdiaglemOLD  20897  psrass1lemOLD  20899  gsumbagdiaglem  20900  psrass1lem  20902  psrass1  20930  mplmonmul  20993  ply1opprmul  21160  coe1mul  21191  2ndcdisj2  22354  fbssfi  22734  isfcf  22931  nmotri  23637  nghmplusg  23638  0nmhm  23653  iundisj2  24446  ovolioo  24465  uniiccdif  24475  basellem9  25971  cplgr2vpr  27521  redwlk  27760  clwwlknccat  28146  frgrwopreglem5a  28394  lnocoi  28838  ipasslem5  28916  hhssabloilem  29342  hhssnv  29345  shscli  29398  shmodsi  29470  lnopmi  30081  lnopcoi  30084  cnlnadjlem2  30149  adjmul  30173  leopmul2i  30216  leoptr  30218  pjimai  30257  mdslle1i  30398  mdslle2i  30399  mdslj1i  30400  mdslj2i  30401  mdslmd1lem1  30406  mdslmd2i  30411  atexch  30462  atcvatlem  30466  chirredlem3  30473  sumdmdii  30496  sumdmdlem  30499  cdj3i  30522  iundisj2f  30648  iundisj2fi  30838  xrge0omnd  31056  srafldlvec  31390  bnj1384  32725  revpfxsfxrev  32790  satffunlem2lem1  33079  cgr3permute3  34086  cgr3permute1  34087  cgr3com  34092  nndivsub  34383  lindsadd  35507  mblfinlem2  35552  cnambfre  35562  ftc1anclem5  35591  fzmul  35636  isismty  35696  heibor1  35705  heiborlem3  35708  hlatjcl  37118  hlatjcom  37119  hlatlej1  37126  hlrelat5N  37152  2lplnmN  37310  2llnmj  37311  2lplnmj  37373  factwoffsmonot  39885  isdomn4  39894  syl3an12  39897  zexpgcd  40044  dvdsexpnn  40048  elmapresaunres2  40296  fzneg  40507  lsmfgcl  40602  trelded  41858  jaoded  41859  el123  42057  suctrALT  42119  suctrALTcf  42215  fnfocofob  44243  ltsubsubaddltsub  44466  fmtnoprmfac2lem1  44691  gboge9  44889  bgoldbtbndlem3  44932  nnsgrp  45044  c0snghm  45147  2zrngALT  45179  nn0sumltlt  45359  lincsum  45443  dignn0fr  45620  dignn0flhalflem2  45635