Theorem syl3an 1159

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  syl2an3an  1421  spc3egv  3602  euelss  4337  3elpr2eq  4910  funtpg  6622  fresaun  6779  fresaunres2  6780  ftpg  7175  eloprabga  7540  eloprabgaOLD  7541  elmapresaun  8918  djuenun  10208  addasspi  10932  mulasspi  10934  distrpi  10935  addcanpi  10936  mulcanpi  10937  ltapi  10940  lemul1  12116  ltdiv2  12151  zletr  12658  zdivadd  12686  eluzsub  12905  nn01to3  12980  qdivcl  13009  maxle  13229  lemin  13230  maxlt  13231  ltmin  13232  xaddass  13287  xmulasslem3  13324  xadddilem  13332  iooneg  13507  zltaddlt1le  13541  fzen  13577  fzaddel  13594  fzadd2  13595  fzrev  13623  fzrevral2  13649  fzshftral  13651  fzosubel2  13760  fzonn0p1p1  13779  fldiv2  13897  modmulnn  13925  modcyc2  13943  prsshashgt1  14445  hashssdif  14447  pfxccatin12lem4  14760  fsum0diag2  15815  binomrisefac  16074  efsub  16132  dvdsnegb  16307  muldvds1  16314  muldvds2  16315  dvdscmul  16316  dvdsmulc  16317  dvdscmulr  16318  dvdsmulcr  16319  dvds2add  16323  dvds2sub  16324  dvdstr  16327  addmodlteqALT  16358  divalglem8  16433  divalgb  16437  divalgmod  16439  ndvdsadd  16443  modgcd  16565  absmulgcd  16582  rpmulgcd  16590  zexpgcd  16598  cncongr2  16701  hashdvds  16808  pythagtriplem1  16849  vdwlem3  17016  ressinbas  17290  gsumws2  18867  mulgmodid  19143  nmzsubg  19195  pmtr3ncomlem1  19505  pmtrdifellem1  19508  subcmn  19869  gexexlem  19884  lsmcom  19890  zaddablx  19904  gsumpr  19987  c0snghm  20480  isdomn4  20732  drngmcl  20766  psgnghm  21615  phlssphl  21694  assa2ass  21900  psrbagconf1o  21966  gsumbagdiaglem  21967  psrass1lem  21969  psrass1  22001  mplmonmul  22071  psdmul  22187  ply1opprmul  22255  coe1mul  22288  2ndcdisj2  23480  fbssfi  23860  isfcf  24057  nmotri  24775  nghmplusg  24776  0nmhm  24791  iundisj2  25597  ovolioo  25616  uniiccdif  25626  basellem9  27146  cplgr2vpr  29464  redwlk  29704  clwwlknccat  30091  frgrwopreglem5a  30339  lnocoi  30785  ipasslem5  30863  hhssabloilem  31289  hhssnv  31292  shscli  31345  shmodsi  31417  lnopmi  32028  lnopcoi  32031  cnlnadjlem2  32096  adjmul  32120  leopmul2i  32163  leoptr  32165  pjimai  32204  mdslle1i  32345  mdslle2i  32346  mdslj1i  32347  mdslj2i  32348  mdslmd1lem1  32353  mdslmd2i  32358  atexch  32409  atcvatlem  32413  chirredlem3  32420  sumdmdii  32443  sumdmdlem  32446  cdj3i  32469  iundisj2f  32609  iundisj2fi  32804  xrge0omnd  33070  srafldlvec  33615  bnj1384  35024  revpfxsfxrev  35099  satffunlem2lem1  35388  cgr3permute3  36028  cgr3permute1  36029  cgr3com  36034  nndivsub  36439  lindsadd  37599  mblfinlem2  37644  cnambfre  37654  ftc1anclem5  37683  fzmul  37727  isismty  37787  heibor1  37796  heiborlem3  37799  hlatjcl  39348  hlatjcom  39349  hlatlej1  39356  hlrelat5N  39383  2lplnmN  39541  2llnmj  39542  2lplnmj  39604  factwoffsmonot  42223  syl3an12  42227  dvdsexpnn  42346  elmapresaunres2  42758  fzneg  42970  lsmfgcl  43062  trelded  44562  jaoded  44563  el123  44761  suctrALT  44823  suctrALTcf  44919  fnfocofob  47028  ltsubsubaddltsub  47250  fmtnoprmfac2lem1  47490  gboge9  47688  bgoldbtbndlem3  47731  usgrgrtrirex  47852  nnsgrp  48020  2zrngALT  48097  nn0sumltlt  48194  lincsum  48274  dignn0fr  48450  dignn0flhalflem2  48465