Theorem syl3an 1178

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl2an3an  1449  3jaao  1460  spc3egv  3557  euelss  4277  3elpr2eq  4833  funtpg  6595  fresaun  6753  fresaunres2  6754  ftpg  7160  eloprabga  7529  elmapresaun  8911  djuenun  10252  addasspi  10983  mulasspi  10985  distrpi  10986  addcanpi  10987  mulcanpi  10988  ltapi  10991  lemul1  12172  ltdiv2  12206  zletr  12743  zdivadd  12773  eluzsub  12998  nn01to3  13071  qdivcl  13101  maxle  13324  lemin  13325  maxlt  13326  ltmin  13327  xaddass  13382  xmulasslem3  13419  xadddilem  13427  iooneg  13605  zltaddlt1le  13639  fzen  13677  fzaddel  13695  fzadd2  13696  fzrev  13724  fzrevral2  13750  fzshftral  13752  fzosubel2  13863  fzonn0p1p1  13882  fldiv2  14004  modmulnn  14032  modcyc2  14050  prsshashgt1  14558  hashssdif  14560  pfxccatin12lem4  14879  revpfxsfxrev  14921  fsum0diag2  15954  binomrisefac  16213  efsub  16273  dvdsnegb  16448  muldvds1  16455  muldvds2  16456  dvdscmul  16457  dvdsmulc  16458  dvdscmulr  16459  dvdsmulcr  16460  dvds2add  16465  dvds2sub  16466  dvdstr  16469  addmodlteqALT  16500  divalglem8  16575  divalgb  16579  divalgmod  16581  ndvdsadd  16585  modgcd  16710  absmulgcd  16727  rpmulgcd  16736  zexpgcd  16744  dvdsexpnn  16745  cncongr2  16848  hashdvds  16957  pythagtriplem1  16999  vdwlem3  17166  ressinbas  17428  gsumws2  19043  mulgmodid  19328  nmzsubg  19380  pmtr3ncomlem1  19692  pmtrdifellem1  19695  subcmn  20056  gexexlem  20071  lsmcom  20077  zaddablx  20091  gsumpr  20174  c0snghm  20699  isdomn4  20972  isdrng3lem2  21011  drngmcl  21014  xrge0omnd  21756  psgnghm  21891  phlssphl  21970  assa2ass  22176  psrbagconf1o  22242  gsumbagdiaglem  22244  psrass1lem  22246  psrass1  22276  mplmonmul  22350  psdmul  22492  ply1opprmul  22561  coe1mul  22594  2ndcdisj2  23781  fbssfi  24161  isfcf  24358  nmotri  25063  nghmplusg  25064  0nmhm  25079  iundisj2  25875  ovolioo  25894  uniiccdif  25904  basellem9  27421  zsoring  28800  cplgr2vpr  30019  redwlk  30256  clwwlknccat  30659  frgrwopreglem5a  30917  lnocoi  31364  ipasslem5  31442  hhssabloilem  31868  hhssnv  31871  shscli  31924  shmodsi  31996  lnopmi  32607  lnopcoi  32610  cnlnadjlem2  32675  adjmul  32699  leopmul2i  32742  leoptr  32744  pjimai  32783  mdslle1i  32924  mdslle2i  32925  mdslj1i  32926  mdslj2i  32927  mdslmd1lem1  32932  mdslmd2i  32937  atexch  32988  atcvatlem  32992  chirredlem3  32999  sumdmdii  33022  sumdmdlem  33025  cdj3i  33048  iundisj2f  33231  iundisj2fi  33435  psrmonmul  34228  srafldlvec  34264  bnj1384  35708  satffunlem2lem1  36255  cgr3permute3  36904  cgr3permute1  36905  cgr3com  36910  nndivsub  37337  lindsadd  38629  mblfinlem2  38669  cnambfre  38679  ftc1anclem5  38708  fzmul  38768  isismty  38828  heibor1  38837  heiborlem3  38840  hlatjcl  40517  hlatjcom  40518  hlatlej1  40525  hlrelat5N  40551  2lplnmN  40709  2llnmj  40710  2lplnmj  40772  syl3an12  43354  elmapresaunres2  43875  fzneg  44082  lsmfgcl  44169  trelded  45641  jaoded  45642  el123  45839  suctrALT  45901  suctrALTcf  45997  fnfocofob  48242  ltsubsubaddltsub  48464  fmtnoprmfac2lem1  48744  gboge9  48955  bgoldbtbndlem3  48998  usgrgrtrirex  49141  gpgedg2iv  49258  nnsgrp  49367  2zrngALT  49444  nn0sumltlt  49555  lincsum  49634  dignn0fr  49806  dignn0flhalflem2  49821