Theorem syl3an 1160

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 1151	. 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  1424  spc3egv  3582  euelss  4307  3elpr2eq  4882  funtpg  6590  fresaun  6748  fresaunres2  6749  ftpg  7145  eloprabga  7514  elmapresaun  8892  djuenun  10183  addasspi  10907  mulasspi  10909  distrpi  10910  addcanpi  10911  mulcanpi  10912  ltapi  10915  lemul1  12091  ltdiv2  12126  zletr  12634  zdivadd  12662  eluzsub  12880  nn01to3  12955  qdivcl  12984  maxle  13205  lemin  13206  maxlt  13207  ltmin  13208  xaddass  13263  xmulasslem3  13300  xadddilem  13308  iooneg  13486  zltaddlt1le  13520  fzen  13556  fzaddel  13573  fzadd2  13574  fzrev  13602  fzrevral2  13628  fzshftral  13630  fzosubel2  13739  fzonn0p1p1  13758  fldiv2  13876  modmulnn  13904  modcyc2  13922  prsshashgt1  14426  hashssdif  14428  pfxccatin12lem4  14742  fsum0diag2  15797  binomrisefac  16056  efsub  16116  dvdsnegb  16291  muldvds1  16298  muldvds2  16299  dvdscmul  16300  dvdsmulc  16301  dvdscmulr  16302  dvdsmulcr  16303  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  16792  pythagtriplem1  16834  vdwlem3  17001  ressinbas  17264  gsumws2  18818  mulgmodid  19094  nmzsubg  19146  pmtr3ncomlem1  19452  pmtrdifellem1  19455  subcmn  19816  gexexlem  19831  lsmcom  19837  zaddablx  19851  gsumpr  19934  c0snghm  20422  isdomn4  20674  drngmcl  20708  psgnghm  21538  phlssphl  21617  assa2ass  21821  psrbagconf1o  21887  gsumbagdiaglem  21888  psrass1lem  21890  psrass1  21922  mplmonmul  21992  psdmul  22102  ply1opprmul  22172  coe1mul  22205  2ndcdisj2  23393  fbssfi  23773  isfcf  23970  nmotri  24676  nghmplusg  24677  0nmhm  24692  iundisj2  25500  ovolioo  25519  uniiccdif  25529  basellem9  27049  cplgr2vpr  29358  redwlk  29598  clwwlknccat  29990  frgrwopreglem5a  30238  lnocoi  30684  ipasslem5  30762  hhssabloilem  31188  hhssnv  31191  shscli  31244  shmodsi  31316  lnopmi  31927  lnopcoi  31930  cnlnadjlem2  31995  adjmul  32019  leopmul2i  32062  leoptr  32064  pjimai  32103  mdslle1i  32244  mdslle2i  32245  mdslj1i  32246  mdslj2i  32247  mdslmd1lem1  32252  mdslmd2i  32257  atexch  32308  atcvatlem  32312  chirredlem3  32319  sumdmdii  32342  sumdmdlem  32345  cdj3i  32368  iundisj2f  32517  iundisj2fi  32720  xrge0omnd  33025  srafldlvec  33572  bnj1384  35009  revpfxsfxrev  35084  satffunlem2lem1  35372  cgr3permute3  36011  cgr3permute1  36012  cgr3com  36017  nndivsub  36421  lindsadd  37583  mblfinlem2  37628  cnambfre  37638  ftc1anclem5  37667  fzmul  37711  isismty  37771  heibor1  37780  heiborlem3  37783  hlatjcl  39331  hlatjcom  39332  hlatlej1  39339  hlrelat5N  39366  2lplnmN  39524  2llnmj  39525  2lplnmj  39587  factwoffsmonot  42201  syl3an12  42206  dvdsexpnn  42329  elmapresaunres2  42741  fzneg  42953  lsmfgcl  43045  trelded  44538  jaoded  44539  el123  44736  suctrALT  44798  suctrALTcf  44894  fnfocofob  47056  ltsubsubaddltsub  47278  fmtnoprmfac2lem1  47528  gboge9  47726  bgoldbtbndlem3  47769  usgrgrtrirex  47910  nnsgrp  48100  2zrngALT  48177  nn0sumltlt  48273  lincsum  48353  dignn0fr  48529  dignn0flhalflem2  48544