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 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  syl2an3an  1423  spc3egv  3594  euelss  4321  3elpr2eq  4907  funtpg  6601  fresaun  6760  fresaunres2  6761  ftpg  7151  eloprabga  7513  eloprabgaOLD  7514  elmapresaun  8871  djuenun  10162  addasspi  10887  mulasspi  10889  distrpi  10890  addcanpi  10891  mulcanpi  10892  ltapi  10895  lemul1  12063  ltdiv2  12097  zletr  12603  zdivadd  12630  eluzsub  12849  nn01to3  12922  qdivcl  12951  maxle  13167  lemin  13168  maxlt  13169  ltmin  13170  xaddass  13225  xmulasslem3  13262  xadddilem  13270  iooneg  13445  zltaddlt1le  13479  fzen  13515  fzaddel  13532  fzadd2  13533  fzrev  13561  fzrevral2  13584  fzshftral  13586  fzosubel2  13689  fzonn0p1p1  13708  fldiv2  13823  modmulnn  13851  modcyc2  13869  prsshashgt1  14367  hashssdif  14369  pfxccatin12lem4  14673  fsum0diag2  15726  binomrisefac  15983  efsub  16040  dvdsnegb  16214  muldvds1  16221  muldvds2  16222  dvdscmul  16223  dvdsmulc  16224  dvdscmulr  16225  dvdsmulcr  16226  dvds2add  16230  dvds2sub  16231  dvdstr  16234  addmodlteqALT  16265  divalglem8  16340  divalgb  16344  divalgmod  16346  ndvdsadd  16350  modgcd  16471  absmulgcd  16488  rpmulgcd  16495  cncongr2  16602  hashdvds  16705  pythagtriplem1  16746  vdwlem3  16913  ressinbas  17187  gsumws2  18720  mulgmodid  18988  nmzsubg  19040  pmtr3ncomlem1  19336  pmtrdifellem1  19339  subcmn  19700  gexexlem  19715  lsmcom  19721  zaddablx  19735  gsumpr  19818  isdomn4  20911  psgnghm  21125  phlssphl  21204  assa2ass  21410  psrbagconf1o  21481  psrbagconf1oOLD  21482  gsumbagdiaglemOLD  21483  psrass1lemOLD  21485  gsumbagdiaglem  21486  psrass1lem  21488  psrass1  21517  mplmonmul  21583  ply1opprmul  21753  coe1mul  21784  2ndcdisj2  22953  fbssfi  23333  isfcf  23530  nmotri  24248  nghmplusg  24249  0nmhm  24264  iundisj2  25058  ovolioo  25077  uniiccdif  25087  basellem9  26583  cplgr2vpr  28680  redwlk  28919  clwwlknccat  29306  frgrwopreglem5a  29554  lnocoi  29998  ipasslem5  30076  hhssabloilem  30502  hhssnv  30505  shscli  30558  shmodsi  30630  lnopmi  31241  lnopcoi  31244  cnlnadjlem2  31309  adjmul  31333  leopmul2i  31376  leoptr  31378  pjimai  31417  mdslle1i  31558  mdslle2i  31559  mdslj1i  31560  mdslj2i  31561  mdslmd1lem1  31566  mdslmd2i  31571  atexch  31622  atcvatlem  31626  chirredlem3  31633  sumdmdii  31656  sumdmdlem  31659  cdj3i  31682  iundisj2f  31809  iundisj2fi  31996  xrge0omnd  32217  srafldlvec  32665  bnj1384  34032  revpfxsfxrev  34095  satffunlem2lem1  34384  cgr3permute3  35008  cgr3permute1  35009  cgr3com  35014  nndivsub  35331  lindsadd  36470  mblfinlem2  36515  cnambfre  36525  ftc1anclem5  36554  fzmul  36598  isismty  36658  heibor1  36667  heiborlem3  36670  hlatjcl  38226  hlatjcom  38227  hlatlej1  38234  hlrelat5N  38261  2lplnmN  38419  2llnmj  38420  2lplnmj  38482  factwoffsmonot  41012  syl3an12  41022  zexpgcd  41223  dvdsexpnn  41227  elmapresaunres2  41495  fzneg  41707  lsmfgcl  41802  trelded  43312  jaoded  43313  el123  43511  suctrALT  43573  suctrALTcf  43669  fnfocofob  45774  ltsubsubaddltsub  45996  fmtnoprmfac2lem1  46221  gboge9  46419  bgoldbtbndlem3  46462  nnsgrp  46574  c0snghm  46701  2zrngALT  46800  nn0sumltlt  46980  lincsum  47064  dignn0fr  47241  dignn0flhalflem2  47256