Theorem syl3an 1158

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  syl2an3an  1420  spc3egv  3532  euelss  4252  3elpr2eq  4835  funtpg  6473  fresaun  6629  fresaunres2  6630  ftpg  7010  eloprabga  7360  eloprabgaOLD  7361  elmapresaun  8626  djuenun  9857  addasspi  10582  mulasspi  10584  distrpi  10585  addcanpi  10586  mulcanpi  10587  ltapi  10590  lemul1  11757  ltdiv2  11791  zletr  12294  zdivadd  12321  nn01to3  12610  qdivcl  12639  maxle  12854  lemin  12855  maxlt  12856  ltmin  12857  xaddass  12912  xmulasslem3  12949  xadddilem  12957  iooneg  13132  zltaddlt1le  13166  fzen  13202  fzaddel  13219  fzadd2  13220  fzrev  13248  fzrevral2  13271  fzshftral  13273  fzosubel2  13375  fzonn0p1p1  13394  fldiv2  13509  modmulnn  13537  modcyc2  13555  prsshashgt1  14053  hashssdif  14055  ccatw2s1assOLD  14269  pfxccatin12lem4  14367  fsum0diag2  15423  binomrisefac  15680  efsub  15737  dvdsnegb  15911  muldvds1  15918  muldvds2  15919  dvdscmul  15920  dvdsmulc  15921  dvdscmulr  15922  dvdsmulcr  15923  dvds2add  15927  dvds2sub  15928  dvdstr  15931  addmodlteqALT  15962  divalglem8  16037  divalgb  16041  divalgmod  16043  ndvdsadd  16047  modgcd  16168  absmulgcd  16185  rpmulgcd  16194  cncongr2  16301  hashdvds  16404  pythagtriplem1  16445  vdwlem3  16612  ressinbas  16881  gsumws2  18396  mulgmodid  18657  nmzsubg  18708  pmtr3ncomlem1  18996  pmtrdifellem1  18999  subcmn  19353  gexexlem  19368  lsmcom  19374  zaddablx  19388  gsumpr  19471  psgnghm  20697  phlssphl  20776  assa2ass  20980  psrbagconf1o  21049  psrbagconf1oOLD  21050  gsumbagdiaglemOLD  21051  psrass1lemOLD  21053  gsumbagdiaglem  21054  psrass1lem  21056  psrass1  21084  mplmonmul  21147  ply1opprmul  21320  coe1mul  21351  2ndcdisj2  22516  fbssfi  22896  isfcf  23093  nmotri  23809  nghmplusg  23810  0nmhm  23825  iundisj2  24618  ovolioo  24637  uniiccdif  24647  basellem9  26143  cplgr2vpr  27703  redwlk  27942  clwwlknccat  28328  frgrwopreglem5a  28576  lnocoi  29020  ipasslem5  29098  hhssabloilem  29524  hhssnv  29527  shscli  29580  shmodsi  29652  lnopmi  30263  lnopcoi  30266  cnlnadjlem2  30331  adjmul  30355  leopmul2i  30398  leoptr  30400  pjimai  30439  mdslle1i  30580  mdslle2i  30581  mdslj1i  30582  mdslj2i  30583  mdslmd1lem1  30588  mdslmd2i  30593  atexch  30644  atcvatlem  30648  chirredlem3  30655  sumdmdii  30678  sumdmdlem  30681  cdj3i  30704  iundisj2f  30830  iundisj2fi  31020  xrge0omnd  31239  srafldlvec  31578  bnj1384  32912  revpfxsfxrev  32977  satffunlem2lem1  33266  cgr3permute3  34276  cgr3permute1  34277  cgr3com  34282  nndivsub  34573  lindsadd  35697  mblfinlem2  35742  cnambfre  35752  ftc1anclem5  35781  fzmul  35826  isismty  35886  heibor1  35895  heiborlem3  35898  hlatjcl  37308  hlatjcom  37309  hlatlej1  37316  hlrelat5N  37342  2lplnmN  37500  2llnmj  37501  2lplnmj  37563  factwoffsmonot  40091  isdomn4  40100  syl3an12  40103  zexpgcd  40257  dvdsexpnn  40261  elmapresaunres2  40509  fzneg  40720  lsmfgcl  40815  trelded  42074  jaoded  42075  el123  42273  suctrALT  42335  suctrALTcf  42431  fnfocofob  44458  ltsubsubaddltsub  44681  fmtnoprmfac2lem1  44906  gboge9  45104  bgoldbtbndlem3  45147  nnsgrp  45259  c0snghm  45362  2zrngALT  45394  nn0sumltlt  45574  lincsum  45658  dignn0fr  45835  dignn0flhalflem2  45850