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  3557  euelss  4284  3elpr2eq  4862  funtpg  6547  fresaun  6705  fresaunres2  6706  ftpg  7101  eloprabga  7467  elmapresaun  8818  djuenun  10081  addasspi  10806  mulasspi  10808  distrpi  10809  addcanpi  10810  mulcanpi  10811  ltapi  10814  lemul1  11993  ltdiv2  12028  zletr  12535  zdivadd  12563  eluzsub  12781  nn01to3  12854  qdivcl  12883  maxle  13106  lemin  13107  maxlt  13108  ltmin  13109  xaddass  13164  xmulasslem3  13201  xadddilem  13209  iooneg  13387  zltaddlt1le  13421  fzen  13457  fzaddel  13474  fzadd2  13475  fzrev  13503  fzrevral2  13529  fzshftral  13531  fzosubel2  13641  fzonn0p1p1  13660  fldiv2  13781  modmulnn  13809  modcyc2  13827  prsshashgt1  14333  hashssdif  14335  pfxccatin12lem4  14649  fsum0diag2  15706  binomrisefac  15965  efsub  16025  dvdsnegb  16200  muldvds1  16207  muldvds2  16208  dvdscmul  16209  dvdsmulc  16210  dvdscmulr  16211  dvdsmulcr  16212  dvds2add  16217  dvds2sub  16218  dvdstr  16221  addmodlteqALT  16252  divalglem8  16327  divalgb  16331  divalgmod  16333  ndvdsadd  16337  modgcd  16459  absmulgcd  16476  rpmulgcd  16484  zexpgcd  16492  cncongr2  16595  hashdvds  16702  pythagtriplem1  16744  vdwlem3  16911  ressinbas  17172  gsumws2  18767  mulgmodid  19043  nmzsubg  19094  pmtr3ncomlem1  19402  pmtrdifellem1  19405  subcmn  19766  gexexlem  19781  lsmcom  19787  zaddablx  19801  gsumpr  19884  c0snghm  20400  isdomn4  20649  drngmcl  20683  xrge0omnd  21400  psgnghm  21535  phlssphl  21614  assa2ass  21818  psrbagconf1o  21885  gsumbagdiaglem  21886  psrass1lem  21888  psrass1  21919  mplmonmul  21991  psdmul  22109  ply1opprmul  22179  coe1mul  22212  2ndcdisj2  23401  fbssfi  23781  isfcf  23978  nmotri  24683  nghmplusg  24684  0nmhm  24699  iundisj2  25506  ovolioo  25525  uniiccdif  25535  basellem9  27055  zsoring  28405  cplgr2vpr  29506  redwlk  29744  clwwlknccat  30138  frgrwopreglem5a  30386  lnocoi  30832  ipasslem5  30910  hhssabloilem  31336  hhssnv  31339  shscli  31392  shmodsi  31464  lnopmi  32075  lnopcoi  32078  cnlnadjlem2  32143  adjmul  32167  leopmul2i  32210  leoptr  32212  pjimai  32251  mdslle1i  32392  mdslle2i  32393  mdslj1i  32394  mdslj2i  32395  mdslmd1lem1  32400  mdslmd2i  32405  atexch  32456  atcvatlem  32460  chirredlem3  32467  sumdmdii  32490  sumdmdlem  32493  cdj3i  32516  iundisj2f  32665  iundisj2fi  32877  srafldlvec  33742  bnj1384  35188  revpfxsfxrev  35310  satffunlem2lem1  35598  cgr3permute3  36241  cgr3permute1  36242  cgr3com  36247  nndivsub  36651  lindsadd  37810  mblfinlem2  37855  cnambfre  37865  ftc1anclem5  37894  fzmul  37938  isismty  37998  heibor1  38007  heiborlem3  38010  hlatjcl  39623  hlatjcom  39624  hlatlej1  39631  hlrelat5N  39657  2lplnmN  39815  2llnmj  39816  2lplnmj  39878  syl3an12  42459  dvdsexpnn  42584  elmapresaunres2  43009  fzneg  43220  lsmfgcl  43312  trelded  44802  jaoded  44803  el123  45000  suctrALT  45062  suctrALTcf  45158  fnfocofob  47321  ltsubsubaddltsub  47543  fmtnoprmfac2lem1  47808  gboge9  48006  bgoldbtbndlem3  48049  usgrgrtrirex  48192  gpgedg2iv  48309  nnsgrp  48419  2zrngALT  48496  nn0sumltlt  48592  lincsum  48671  dignn0fr  48843  dignn0flhalflem2  48858