Theorem syl3an 1161

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 1152	. 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  1424  spc3egv  3603  euelss  4332  3elpr2eq  4906  funtpg  6621  fresaun  6779  fresaunres2  6780  ftpg  7176  eloprabga  7542  elmapresaun  8920  djuenun  10211  addasspi  10935  mulasspi  10937  distrpi  10938  addcanpi  10939  mulcanpi  10940  ltapi  10943  lemul1  12119  ltdiv2  12154  zletr  12661  zdivadd  12689  eluzsub  12908  nn01to3  12983  qdivcl  13012  maxle  13233  lemin  13234  maxlt  13235  ltmin  13236  xaddass  13291  xmulasslem3  13328  xadddilem  13336  iooneg  13511  zltaddlt1le  13545  fzen  13581  fzaddel  13598  fzadd2  13599  fzrev  13627  fzrevral2  13653  fzshftral  13655  fzosubel2  13764  fzonn0p1p1  13783  fldiv2  13901  modmulnn  13929  modcyc2  13947  prsshashgt1  14449  hashssdif  14451  pfxccatin12lem4  14764  fsum0diag2  15819  binomrisefac  16078  efsub  16136  dvdsnegb  16311  muldvds1  16318  muldvds2  16319  dvdscmul  16320  dvdsmulc  16321  dvdscmulr  16322  dvdsmulcr  16323  dvds2add  16327  dvds2sub  16328  dvdstr  16331  addmodlteqALT  16362  divalglem8  16437  divalgb  16441  divalgmod  16443  ndvdsadd  16447  modgcd  16569  absmulgcd  16586  rpmulgcd  16594  zexpgcd  16602  cncongr2  16705  hashdvds  16812  pythagtriplem1  16854  vdwlem3  17021  ressinbas  17291  gsumws2  18855  mulgmodid  19131  nmzsubg  19183  pmtr3ncomlem1  19491  pmtrdifellem1  19494  subcmn  19855  gexexlem  19870  lsmcom  19876  zaddablx  19890  gsumpr  19973  c0snghm  20464  isdomn4  20716  drngmcl  20750  psgnghm  21598  phlssphl  21677  assa2ass  21883  psrbagconf1o  21949  gsumbagdiaglem  21950  psrass1lem  21952  psrass1  21984  mplmonmul  22054  psdmul  22170  ply1opprmul  22240  coe1mul  22273  2ndcdisj2  23465  fbssfi  23845  isfcf  24042  nmotri  24760  nghmplusg  24761  0nmhm  24776  iundisj2  25584  ovolioo  25603  uniiccdif  25613  basellem9  27132  cplgr2vpr  29450  redwlk  29690  clwwlknccat  30082  frgrwopreglem5a  30330  lnocoi  30776  ipasslem5  30854  hhssabloilem  31280  hhssnv  31283  shscli  31336  shmodsi  31408  lnopmi  32019  lnopcoi  32022  cnlnadjlem2  32087  adjmul  32111  leopmul2i  32154  leoptr  32156  pjimai  32195  mdslle1i  32336  mdslle2i  32337  mdslj1i  32338  mdslj2i  32339  mdslmd1lem1  32344  mdslmd2i  32349  atexch  32400  atcvatlem  32404  chirredlem3  32411  sumdmdii  32434  sumdmdlem  32437  cdj3i  32460  iundisj2f  32603  iundisj2fi  32799  xrge0omnd  33088  srafldlvec  33637  bnj1384  35046  revpfxsfxrev  35121  satffunlem2lem1  35409  cgr3permute3  36048  cgr3permute1  36049  cgr3com  36054  nndivsub  36458  lindsadd  37620  mblfinlem2  37665  cnambfre  37675  ftc1anclem5  37704  fzmul  37748  isismty  37808  heibor1  37817  heiborlem3  37820  hlatjcl  39368  hlatjcom  39369  hlatlej1  39376  hlrelat5N  39403  2lplnmN  39561  2llnmj  39562  2lplnmj  39624  factwoffsmonot  42243  syl3an12  42248  dvdsexpnn  42368  elmapresaunres2  42782  fzneg  42994  lsmfgcl  43086  trelded  44585  jaoded  44586  el123  44784  suctrALT  44846  suctrALTcf  44942  fnfocofob  47091  ltsubsubaddltsub  47313  fmtnoprmfac2lem1  47553  gboge9  47751  bgoldbtbndlem3  47794  usgrgrtrirex  47917  nnsgrp  48093  2zrngALT  48170  nn0sumltlt  48266  lincsum  48346  dignn0fr  48522  dignn0flhalflem2  48537