Theorem syl3an 1178

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl2an3an  1449  3jaao  1460  spc3egv  3565  euelss  4288  3elpr2eq  4876  funtpg  6598  fresaun  6756  fresaunres2  6757  ftpg  7160  eloprabga  7532  elmapresaun  8887  djuenun  10173  addasspi  10898  mulasspi  10900  distrpi  10901  addcanpi  10902  mulcanpi  10903  ltapi  10906  lemul1  12085  ltdiv2  12119  zletr  12656  zdivadd  12685  eluzsub  12910  nn01to3  12983  qdivcl  13012  maxle  13235  lemin  13236  maxlt  13237  ltmin  13238  xaddass  13293  xmulasslem3  13330  xadddilem  13338  iooneg  13516  zltaddlt1le  13550  fzen  13587  fzaddel  13605  fzadd2  13606  fzrev  13634  fzrevral2  13660  fzshftral  13662  fzosubel2  13773  fzonn0p1p1  13792  fldiv2  13914  modmulnn  13942  modcyc2  13960  prsshashgt1  14467  hashssdif  14469  pfxccatin12lem4  14787  revpfxsfxrev  14829  fsum0diag2  15860  binomrisefac  16121  efsub  16181  dvdsnegb  16356  muldvds1  16363  muldvds2  16364  dvdscmul  16365  dvdsmulc  16366  dvdscmulr  16367  dvdsmulcr  16368  dvds2add  16373  dvds2sub  16374  dvdstr  16377  addmodlteqALT  16408  divalglem8  16483  divalgb  16487  divalgmod  16489  ndvdsadd  16493  modgcd  16615  absmulgcd  16632  rpmulgcd  16640  zexpgcd  16648  cncongr2  16751  hashdvds  16859  pythagtriplem1  16901  vdwlem3  17068  ressinbas  17330  gsumws2  18932  mulgmodid  19210  nmzsubg  19262  pmtr3ncomlem1  19574  pmtrdifellem1  19577  subcmn  19938  gexexlem  19953  lsmcom  19959  zaddablx  19973  gsumpr  20056  c0snghm  20579  isdomn4  20851  isdrng3lem2  20889  drngmcl  20892  xrge0omnd  21632  psgnghm  21767  phlssphl  21846  assa2ass  22050  psrbagconf1o  22116  gsumbagdiaglem  22118  psrass1lem  22120  psrass1  22150  mplmonmul  22224  psdmul  22366  ply1opprmul  22435  coe1mul  22468  2ndcdisj2  23651  fbssfi  24031  isfcf  24228  nmotri  24933  nghmplusg  24934  0nmhm  24949  iundisj2  25745  ovolioo  25764  uniiccdif  25774  basellem9  27290  zsoring  28639  cplgr2vpr  29820  redwlk  30057  clwwlknccat  30451  frgrwopreglem5a  30699  lnocoi  31146  ipasslem5  31224  hhssabloilem  31650  hhssnv  31653  shscli  31706  shmodsi  31778  lnopmi  32389  lnopcoi  32392  cnlnadjlem2  32457  adjmul  32481  leopmul2i  32524  leoptr  32526  pjimai  32565  mdslle1i  32706  mdslle2i  32707  mdslj1i  32708  mdslj2i  32709  mdslmd1lem1  32714  mdslmd2i  32719  atexch  32770  atcvatlem  32774  chirredlem3  32781  sumdmdii  32804  sumdmdlem  32807  cdj3i  32830  iundisj2f  32972  iundisj2fi  33179  psrmonmul  33971  srafldlvec  34007  bnj1384  35452  satffunlem2lem1  35917  cgr3permute3  36560  cgr3permute1  36561  cgr3com  36566  nndivsub  37009  lindsadd  38305  mblfinlem2  38350  cnambfre  38360  ftc1anclem5  38389  fzmul  38433  isismty  38493  heibor1  38502  heiborlem3  38505  hlatjcl  40182  hlatjcom  40183  hlatlej1  40190  hlrelat5N  40216  2lplnmN  40374  2llnmj  40375  2lplnmj  40437  syl3an12  43019  dvdsexpnn  43135  elmapresaunres2  43543  fzneg  43750  lsmfgcl  43842  trelded  45315  jaoded  45316  el123  45513  suctrALT  45575  suctrALTcf  45671  fnfocofob  47857  ltsubsubaddltsub  48079  fmtnoprmfac2lem1  48359  gboge9  48570  bgoldbtbndlem3  48613  usgrgrtrirex  48756  gpgedg2iv  48873  nnsgrp  48983  2zrngALT  49060  nn0sumltlt  49171  lincsum  49250  dignn0fr  49422  dignn0flhalflem2  49437