Theorem syl3an 1172

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

Syntax hints:   → wi 4   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  syl2an3an  1440  3jaao  1452  spc3egv  3562  euelss  4284  3elpr2eq  4863  funtpg  6572  fresaun  6731  fresaunres2  6732  ftpg  7135  eloprabga  7501  elmapresaun  8858  djuenun  10124  addasspi  10850  mulasspi  10852  distrpi  10853  addcanpi  10854  mulcanpi  10855  ltapi  10858  lemul1  12040  ltdiv2  12075  zletr  12612  zdivadd  12641  eluzsub  12866  nn01to3  12939  qdivcl  12968  maxle  13191  lemin  13192  maxlt  13193  ltmin  13194  xaddass  13249  xmulasslem3  13286  xadddilem  13294  iooneg  13472  zltaddlt1le  13506  fzen  13543  fzaddel  13560  fzadd2  13561  fzrev  13589  fzrevral2  13615  fzshftral  13617  fzosubel2  13728  fzonn0p1p1  13747  fldiv2  13868  modmulnn  13896  modcyc2  13914  prsshashgt1  14420  hashssdif  14422  pfxccatin12lem4  14736  fsum0diag2  15793  binomrisefac  16055  efsub  16115  dvdsnegb  16290  muldvds1  16297  muldvds2  16298  dvdscmul  16299  dvdsmulc  16300  dvdscmulr  16301  dvdsmulcr  16302  dvds2add  16307  dvds2sub  16308  dvdstr  16311  addmodlteqALT  16342  divalglem8  16417  divalgb  16421  divalgmod  16423  ndvdsadd  16427  modgcd  16549  absmulgcd  16566  rpmulgcd  16574  zexpgcd  16582  cncongr2  16685  hashdvds  16793  pythagtriplem1  16835  vdwlem3  17002  ressinbas  17264  gsumws2  18859  mulgmodid  19138  nmzsubg  19189  pmtr3ncomlem1  19496  pmtrdifellem1  19499  subcmn  19860  gexexlem  19875  lsmcom  19881  zaddablx  19895  gsumpr  19978  c0snghm  20492  isdomn4  20745  drngmcl  20779  xrge0omnd  21477  psgnghm  21612  phlssphl  21691  assa2ass  21895  psrbagconf1o  21961  gsumbagdiaglem  21963  psrass1lem  21965  psrass1  21995  mplmonmul  22069  psdmul  22211  ply1opprmul  22280  coe1mul  22313  2ndcdisj2  23497  fbssfi  23877  isfcf  24074  nmotri  24779  nghmplusg  24780  0nmhm  24795  iundisj2  25591  ovolioo  25610  uniiccdif  25620  basellem9  27130  zsoring  28479  cplgr2vpr  29580  redwlk  29817  clwwlknccat  30211  frgrwopreglem5a  30459  lnocoi  30906  ipasslem5  30984  hhssabloilem  31410  hhssnv  31413  shscli  31466  shmodsi  31538  lnopmi  32149  lnopcoi  32152  cnlnadjlem2  32217  adjmul  32241  leopmul2i  32284  leoptr  32286  pjimai  32325  mdslle1i  32466  mdslle2i  32467  mdslj1i  32468  mdslj2i  32469  mdslmd1lem1  32474  mdslmd2i  32479  atexch  32530  atcvatlem  32534  chirredlem3  32541  sumdmdii  32564  sumdmdlem  32567  cdj3i  32590  iundisj2f  32739  iundisj2fi  32949  psrmonmul  33808  srafldlvec  33844  bnj1384  35291  revpfxsfxrev  35430  satffunlem2lem1  35718  cgr3permute3  36361  cgr3permute1  36362  cgr3com  36367  nndivsub  36781  lindsadd  38076  mblfinlem2  38121  cnambfre  38131  ftc1anclem5  38160  fzmul  38204  isismty  38264  heibor1  38273  heiborlem3  38276  hlatjcl  39955  hlatjcom  39956  hlatlej1  39963  hlrelat5N  39989  2lplnmN  40147  2llnmj  40148  2lplnmj  40210  syl3an12  42790  dvdsexpnn  42906  elmapresaunres2  43316  fzneg  43523  lsmfgcl  43615  trelded  45105  jaoded  45106  el123  45303  suctrALT  45365  suctrALTcf  45461  fnfocofob  47637  ltsubsubaddltsub  47859  fmtnoprmfac2lem1  48139  gboge9  48350  bgoldbtbndlem3  48393  usgrgrtrirex  48536  gpgedg2iv  48653  nnsgrp  48763  2zrngALT  48840  nn0sumltlt  48936  lincsum  49015  dignn0fr  49187  dignn0flhalflem2  49202