Theorem syl3an 1153

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 1144	. 2 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → (𝜓 ∧ 𝜃 ∧ 𝜂))
5		syl3an.4	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) → 𝜁)
6	4, 5	syl 17	1 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)

Syntax hints:   → wi 4   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  syl2an3an  1415  spc3egv  3546  euelss  4210  3elpr2eq  4744  funtpg  6279  fresaun  6417  fresaunres2  6418  ftpg  6781  eloprabga  7117  elmapresaun  8294  djuenun  9442  addasspi  10163  mulasspi  10165  distrpi  10166  addcanpi  10167  mulcanpi  10168  ltapi  10171  lemul1  11340  ltdiv2  11374  zletr  11875  zdivadd  11902  nn01to3  12190  qdivcl  12219  maxle  12434  lemin  12435  maxlt  12436  ltmin  12437  xaddass  12492  xmulasslem3  12529  xadddilem  12537  iooneg  12707  zltaddlt1le  12740  fzen  12774  fzaddel  12791  fzadd2  12792  fzrev  12820  fzrevral2  12843  fzshftral  12845  fzosubel2  12947  fzonn0p1p1  12966  fldiv2  13079  modmulnn  13107  modcyc2  13125  prsshashgt1  13619  hashssdif  13621  ccatsymb  13780  ccatw2s1ass  13829  pfxccatin12lem4  13924  fsum0diag2  14971  binomrisefac  15229  efsub  15286  dvdsnegb  15460  muldvds1  15467  muldvds2  15468  dvdscmul  15469  dvdsmulc  15470  dvdscmulr  15471  dvdsmulcr  15472  dvds2add  15476  dvds2sub  15477  dvdstr  15479  addmodlteqALT  15508  divalglem8  15584  divalgb  15588  divalgmod  15590  ndvdsadd  15594  modgcd  15713  absmulgcd  15726  rpmulgcd  15735  cncongr2  15841  hashdvds  15941  pythagtriplem1  15982  vdwlem3  16148  ressinbas  16389  gsumws2  17818  mulgmodid  18020  nmzsubg  18074  pmtr3ncomlem1  18332  pmtrdifellem1  18335  subcmn  18682  gexexlem  18695  lsmcom  18701  zaddablx  18715  gsumpr  18795  assa2ass  19784  psrbagconf1o  19842  gsumbagdiaglem  19843  psrass1lem  19845  psrass1  19873  mplmonmul  19932  ply1opprmul  20090  coe1mul  20121  psgnghm  20406  phlssphl  20485  2ndcdisj2  21749  fbssfi  22129  isfcf  22326  nmotri  23031  nghmplusg  23032  0nmhm  23047  iundisj2  23833  ovolioo  23852  uniiccdif  23862  basellem9  25348  cplgr2vpr  26898  redwlk  27139  clwwlknccat  27529  frgrwopreglem5a  27782  lnocoi  28225  ipasslem5  28303  hhssabloilem  28729  hhssnv  28732  shscli  28785  shmodsi  28857  lnopmi  29468  lnopcoi  29471  cnlnadjlem2  29536  adjmul  29560  leopmul2i  29603  leoptr  29605  pjimai  29644  mdslle1i  29785  mdslle2i  29786  mdslj1i  29787  mdslj2i  29788  mdslmd1lem1  29793  mdslmd2i  29798  atexch  29849  atcvatlem  29853  chirredlem3  29860  sumdmdii  29883  sumdmdlem  29886  cdj3i  29909  iundisj2f  30030  iundisj2fi  30206  xrge0omnd  30372  srafldlvec  30595  bnj1384  31918  satffunlem2lem1  32259  noetalem5  32830  cgr3permute3  33117  cgr3permute1  33118  cgr3com  33123  nndivsub  33414  lindsadd  34416  mblfinlem2  34461  cnambfre  34471  ftc1anclem5  34502  fzmul  34548  isismty  34611  heibor1  34620  heiborlem3  34623  hlatjcl  36034  hlatjcom  36035  hlatlej1  36042  hlrelat5N  36068  2lplnmN  36226  2llnmj  36227  2lplnmj  36289  zexpgcd  38707  elmapresaunres2  38853  fzneg  39064  lsmfgcl  39159  trelded  40438  jaoded  40439  el123  40637  suctrALT  40699  suctrALTcf  40795  ltsubsubaddltsub  43017  fmtnoprmfac2lem1  43210  gboge9  43411  bgoldbtbndlem3  43454  nnsgrp  43566  c0snghm  43665  2zrngALT  43697  nn0sumltlt  43876  lincsum  43964  dignn0fr  44142  dignn0flhalflem2  44157