Theorem syl3an 1176

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  syl2an3an  1445  3jaao  1456  spc3egv  3565  euelss  4287  3elpr2eq  4867  funtpg  6580  fresaun  6739  fresaunres2  6740  ftpg  7143  eloprabga  7509  elmapresaun  8866  djuenun  10142  addasspi  10868  mulasspi  10870  distrpi  10871  addcanpi  10872  mulcanpi  10873  ltapi  10876  lemul1  12058  ltdiv2  12092  zletr  12629  zdivadd  12658  eluzsub  12883  nn01to3  12956  qdivcl  12985  maxle  13208  lemin  13209  maxlt  13210  ltmin  13211  xaddass  13266  xmulasslem3  13303  xadddilem  13311  iooneg  13489  zltaddlt1le  13523  fzen  13560  fzaddel  13577  fzadd2  13578  fzrev  13606  fzrevral2  13632  fzshftral  13634  fzosubel2  13745  fzonn0p1p1  13764  fldiv2  13885  modmulnn  13913  modcyc2  13931  prsshashgt1  14437  hashssdif  14439  pfxccatin12lem4  14753  fsum0diag2  15824  binomrisefac  16086  efsub  16146  dvdsnegb  16321  muldvds1  16328  muldvds2  16329  dvdscmul  16330  dvdsmulc  16331  dvdscmulr  16332  dvdsmulcr  16333  dvds2add  16338  dvds2sub  16339  dvdstr  16342  addmodlteqALT  16373  divalglem8  16448  divalgb  16452  divalgmod  16454  ndvdsadd  16458  modgcd  16580  absmulgcd  16597  rpmulgcd  16605  zexpgcd  16613  cncongr2  16716  hashdvds  16824  pythagtriplem1  16866  vdwlem3  17033  ressinbas  17295  gsumws2  18891  mulgmodid  19170  nmzsubg  19222  pmtr3ncomlem1  19534  pmtrdifellem1  19537  subcmn  19898  gexexlem  19913  lsmcom  19919  zaddablx  19933  gsumpr  20016  c0snghm  20537  isdomn4  20791  drngmcl  20825  xrge0omnd  21555  psgnghm  21690  phlssphl  21769  assa2ass  21973  psrbagconf1o  22039  gsumbagdiaglem  22041  psrass1lem  22043  psrass1  22073  mplmonmul  22147  psdmul  22289  ply1opprmul  22358  coe1mul  22391  2ndcdisj2  23575  fbssfi  23955  isfcf  24152  nmotri  24857  nghmplusg  24858  0nmhm  24873  iundisj2  25669  ovolioo  25688  uniiccdif  25698  basellem9  27211  zsoring  28560  cplgr2vpr  29692  redwlk  29929  clwwlknccat  30323  frgrwopreglem5a  30571  lnocoi  31018  ipasslem5  31096  hhssabloilem  31522  hhssnv  31525  shscli  31578  shmodsi  31650  lnopmi  32261  lnopcoi  32264  cnlnadjlem2  32329  adjmul  32353  leopmul2i  32396  leoptr  32398  pjimai  32437  mdslle1i  32578  mdslle2i  32579  mdslj1i  32580  mdslj2i  32581  mdslmd1lem1  32586  mdslmd2i  32591  atexch  32642  atcvatlem  32646  chirredlem3  32653  sumdmdii  32676  sumdmdlem  32679  cdj3i  32702  iundisj2f  32845  iundisj2fi  33054  psrmonmul  33857  srafldlvec  33893  bnj1384  35337  revpfxsfxrev  35478  satffunlem2lem1  35767  cgr3permute3  36410  cgr3permute1  36411  cgr3com  36416  nndivsub  36830  lindsadd  38124  mblfinlem2  38169  cnambfre  38179  ftc1anclem5  38208  fzmul  38252  isismty  38312  heibor1  38321  heiborlem3  38324  hlatjcl  40003  hlatjcom  40004  hlatlej1  40011  hlrelat5N  40037  2lplnmN  40195  2llnmj  40196  2lplnmj  40258  syl3an12  42838  dvdsexpnn  42954  elmapresaunres2  43364  fzneg  43571  lsmfgcl  43663  trelded  45139  jaoded  45140  el123  45337  suctrALT  45399  suctrALTcf  45495  fnfocofob  47671  ltsubsubaddltsub  47893  fmtnoprmfac2lem1  48173  gboge9  48384  bgoldbtbndlem3  48427  usgrgrtrirex  48570  gpgedg2iv  48687  nnsgrp  48797  2zrngALT  48874  nn0sumltlt  48981  lincsum  49060  dignn0fr  49232  dignn0flhalflem2  49247