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  1425  spc3egv  3559  euelss  4286  3elpr2eq  4864  funtpg  6555  fresaun  6713  fresaunres2  6714  ftpg  7111  eloprabga  7477  elmapresaun  8830  djuenun  10093  addasspi  10818  mulasspi  10820  distrpi  10821  addcanpi  10822  mulcanpi  10823  ltapi  10826  lemul1  12005  ltdiv2  12040  zletr  12547  zdivadd  12575  eluzsub  12793  nn01to3  12866  qdivcl  12895  maxle  13118  lemin  13119  maxlt  13120  ltmin  13121  xaddass  13176  xmulasslem3  13213  xadddilem  13221  iooneg  13399  zltaddlt1le  13433  fzen  13469  fzaddel  13486  fzadd2  13487  fzrev  13515  fzrevral2  13541  fzshftral  13543  fzosubel2  13653  fzonn0p1p1  13672  fldiv2  13793  modmulnn  13821  modcyc2  13839  prsshashgt1  14345  hashssdif  14347  pfxccatin12lem4  14661  fsum0diag2  15718  binomrisefac  15977  efsub  16037  dvdsnegb  16212  muldvds1  16219  muldvds2  16220  dvdscmul  16221  dvdsmulc  16222  dvdscmulr  16223  dvdsmulcr  16224  dvds2add  16229  dvds2sub  16230  dvdstr  16233  addmodlteqALT  16264  divalglem8  16339  divalgb  16343  divalgmod  16345  ndvdsadd  16349  modgcd  16471  absmulgcd  16488  rpmulgcd  16496  zexpgcd  16504  cncongr2  16607  hashdvds  16714  pythagtriplem1  16756  vdwlem3  16923  ressinbas  17184  gsumws2  18779  mulgmodid  19055  nmzsubg  19106  pmtr3ncomlem1  19414  pmtrdifellem1  19417  subcmn  19778  gexexlem  19793  lsmcom  19799  zaddablx  19813  gsumpr  19896  c0snghm  20412  isdomn4  20661  drngmcl  20695  xrge0omnd  21412  psgnghm  21547  phlssphl  21626  assa2ass  21830  psrbagconf1o  21897  gsumbagdiaglem  21898  psrass1lem  21900  psrass1  21931  mplmonmul  22003  psdmul  22121  ply1opprmul  22191  coe1mul  22224  2ndcdisj2  23413  fbssfi  23793  isfcf  23990  nmotri  24695  nghmplusg  24696  0nmhm  24711  iundisj2  25518  ovolioo  25537  uniiccdif  25547  basellem9  27067  zsoring  28417  cplgr2vpr  29518  redwlk  29756  clwwlknccat  30150  frgrwopreglem5a  30398  lnocoi  30844  ipasslem5  30922  hhssabloilem  31348  hhssnv  31351  shscli  31404  shmodsi  31476  lnopmi  32087  lnopcoi  32090  cnlnadjlem2  32155  adjmul  32179  leopmul2i  32222  leoptr  32224  pjimai  32263  mdslle1i  32404  mdslle2i  32405  mdslj1i  32406  mdslj2i  32407  mdslmd1lem1  32412  mdslmd2i  32417  atexch  32468  atcvatlem  32472  chirredlem3  32479  sumdmdii  32502  sumdmdlem  32505  cdj3i  32528  iundisj2f  32676  iundisj2fi  32887  psrmonmul  33726  srafldlvec  33762  bnj1384  35207  revpfxsfxrev  35329  satffunlem2lem1  35617  cgr3permute3  36260  cgr3permute1  36261  cgr3com  36266  nndivsub  36670  lindsadd  37858  mblfinlem2  37903  cnambfre  37913  ftc1anclem5  37942  fzmul  37986  isismty  38046  heibor1  38055  heiborlem3  38058  hlatjcl  39737  hlatjcom  39738  hlatlej1  39745  hlrelat5N  39771  2lplnmN  39929  2llnmj  39930  2lplnmj  39992  syl3an12  42573  dvdsexpnn  42697  elmapresaunres2  43122  fzneg  43333  lsmfgcl  43425  trelded  44915  jaoded  44916  el123  45113  suctrALT  45175  suctrALTcf  45271  fnfocofob  47433  ltsubsubaddltsub  47655  fmtnoprmfac2lem1  47920  gboge9  48118  bgoldbtbndlem3  48161  usgrgrtrirex  48304  gpgedg2iv  48421  nnsgrp  48531  2zrngALT  48608  nn0sumltlt  48704  lincsum  48783  dignn0fr  48955  dignn0flhalflem2  48970