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  3554  euelss  4281  3elpr2eq  4857  funtpg  6541  fresaun  6699  fresaunres2  6700  ftpg  7095  eloprabga  7461  elmapresaun  8810  djuenun  10069  addasspi  10793  mulasspi  10795  distrpi  10796  addcanpi  10797  mulcanpi  10798  ltapi  10801  lemul1  11980  ltdiv2  12015  zletr  12522  zdivadd  12550  eluzsub  12768  nn01to3  12841  qdivcl  12870  maxle  13092  lemin  13093  maxlt  13094  ltmin  13095  xaddass  13150  xmulasslem3  13187  xadddilem  13195  iooneg  13373  zltaddlt1le  13407  fzen  13443  fzaddel  13460  fzadd2  13461  fzrev  13489  fzrevral2  13515  fzshftral  13517  fzosubel2  13627  fzonn0p1p1  13646  fldiv2  13767  modmulnn  13795  modcyc2  13813  prsshashgt1  14319  hashssdif  14321  pfxccatin12lem4  14635  fsum0diag2  15692  binomrisefac  15951  efsub  16011  dvdsnegb  16186  muldvds1  16193  muldvds2  16194  dvdscmul  16195  dvdsmulc  16196  dvdscmulr  16197  dvdsmulcr  16198  dvds2add  16203  dvds2sub  16204  dvdstr  16207  addmodlteqALT  16238  divalglem8  16313  divalgb  16317  divalgmod  16319  ndvdsadd  16323  modgcd  16445  absmulgcd  16462  rpmulgcd  16470  zexpgcd  16478  cncongr2  16581  hashdvds  16688  pythagtriplem1  16730  vdwlem3  16897  ressinbas  17158  gsumws2  18752  mulgmodid  19028  nmzsubg  19079  pmtr3ncomlem1  19387  pmtrdifellem1  19390  subcmn  19751  gexexlem  19766  lsmcom  19772  zaddablx  19786  gsumpr  19869  c0snghm  20384  isdomn4  20633  drngmcl  20667  xrge0omnd  21384  psgnghm  21519  phlssphl  21598  assa2ass  21802  psrbagconf1o  21868  gsumbagdiaglem  21869  psrass1lem  21871  psrass1  21902  mplmonmul  21972  psdmul  22082  ply1opprmul  22152  coe1mul  22185  2ndcdisj2  23373  fbssfi  23753  isfcf  23950  nmotri  24655  nghmplusg  24656  0nmhm  24671  iundisj2  25478  ovolioo  25497  uniiccdif  25507  basellem9  27027  zsoring  28333  cplgr2vpr  29413  redwlk  29651  clwwlknccat  30045  frgrwopreglem5a  30293  lnocoi  30739  ipasslem5  30817  hhssabloilem  31243  hhssnv  31246  shscli  31299  shmodsi  31371  lnopmi  31982  lnopcoi  31985  cnlnadjlem2  32050  adjmul  32074  leopmul2i  32117  leoptr  32119  pjimai  32158  mdslle1i  32299  mdslle2i  32300  mdslj1i  32301  mdslj2i  32302  mdslmd1lem1  32307  mdslmd2i  32312  atexch  32363  atcvatlem  32367  chirredlem3  32374  sumdmdii  32397  sumdmdlem  32400  cdj3i  32423  iundisj2f  32572  iundisj2fi  32784  srafldlvec  33619  bnj1384  35065  revpfxsfxrev  35181  satffunlem2lem1  35469  cgr3permute3  36112  cgr3permute1  36113  cgr3com  36118  nndivsub  36522  lindsadd  37673  mblfinlem2  37718  cnambfre  37728  ftc1anclem5  37757  fzmul  37801  isismty  37861  heibor1  37870  heiborlem3  37873  hlatjcl  39486  hlatjcom  39487  hlatlej1  39494  hlrelat5N  39520  2lplnmN  39678  2llnmj  39679  2lplnmj  39741  syl3an12  42322  dvdsexpnn  42451  elmapresaunres2  42888  fzneg  43099  lsmfgcl  43191  trelded  44682  jaoded  44683  el123  44880  suctrALT  44942  suctrALTcf  45038  fnfocofob  47203  ltsubsubaddltsub  47425  fmtnoprmfac2lem1  47690  gboge9  47888  bgoldbtbndlem3  47931  usgrgrtrirex  48074  gpgedg2iv  48191  nnsgrp  48301  2zrngALT  48378  nn0sumltlt  48474  lincsum  48554  dignn0fr  48726  dignn0flhalflem2  48741