Theorem syl3an 1161

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  syl2an3an  1425  spc3egv  3545  euelss  4272  3elpr2eq  4849  funtpg  6553  fresaun  6711  fresaunres2  6712  ftpg  7110  eloprabga  7476  elmapresaun  8828  djuenun  10093  addasspi  10818  mulasspi  10820  distrpi  10821  addcanpi  10822  mulcanpi  10823  ltapi  10826  lemul1  12007  ltdiv2  12042  zletr  12571  zdivadd  12600  eluzsub  12818  nn01to3  12891  qdivcl  12920  maxle  13143  lemin  13144  maxlt  13145  ltmin  13146  xaddass  13201  xmulasslem3  13238  xadddilem  13246  iooneg  13424  zltaddlt1le  13458  fzen  13495  fzaddel  13512  fzadd2  13513  fzrev  13541  fzrevral2  13567  fzshftral  13569  fzosubel2  13680  fzonn0p1p1  13699  fldiv2  13820  modmulnn  13848  modcyc2  13866  prsshashgt1  14372  hashssdif  14374  pfxccatin12lem4  14688  fsum0diag2  15745  binomrisefac  16007  efsub  16067  dvdsnegb  16242  muldvds1  16249  muldvds2  16250  dvdscmul  16251  dvdsmulc  16252  dvdscmulr  16253  dvdsmulcr  16254  dvds2add  16259  dvds2sub  16260  dvdstr  16263  addmodlteqALT  16294  divalglem8  16369  divalgb  16373  divalgmod  16375  ndvdsadd  16379  modgcd  16501  absmulgcd  16518  rpmulgcd  16526  zexpgcd  16534  cncongr2  16637  hashdvds  16745  pythagtriplem1  16787  vdwlem3  16954  ressinbas  17215  gsumws2  18810  mulgmodid  19089  nmzsubg  19140  pmtr3ncomlem1  19448  pmtrdifellem1  19451  subcmn  19812  gexexlem  19827  lsmcom  19833  zaddablx  19847  gsumpr  19930  c0snghm  20444  isdomn4  20693  drngmcl  20727  xrge0omnd  21425  psgnghm  21560  phlssphl  21639  assa2ass  21843  psrbagconf1o  21909  gsumbagdiaglem  21910  psrass1lem  21912  psrass1  21942  mplmonmul  22014  psdmul  22132  ply1opprmul  22202  coe1mul  22235  2ndcdisj2  23422  fbssfi  23802  isfcf  23999  nmotri  24704  nghmplusg  24705  0nmhm  24720  iundisj2  25516  ovolioo  25535  uniiccdif  25545  basellem9  27052  zsoring  28401  cplgr2vpr  29502  redwlk  29739  clwwlknccat  30133  frgrwopreglem5a  30381  lnocoi  30828  ipasslem5  30906  hhssabloilem  31332  hhssnv  31335  shscli  31388  shmodsi  31460  lnopmi  32071  lnopcoi  32074  cnlnadjlem2  32139  adjmul  32163  leopmul2i  32206  leoptr  32208  pjimai  32247  mdslle1i  32388  mdslle2i  32389  mdslj1i  32390  mdslj2i  32391  mdslmd1lem1  32396  mdslmd2i  32401  atexch  32452  atcvatlem  32456  chirredlem3  32463  sumdmdii  32486  sumdmdlem  32489  cdj3i  32512  iundisj2f  32660  iundisj2fi  32870  psrmonmul  33694  srafldlvec  33730  bnj1384  35174  revpfxsfxrev  35298  satffunlem2lem1  35586  cgr3permute3  36229  cgr3permute1  36230  cgr3com  36235  nndivsub  36639  lindsadd  37934  mblfinlem2  37979  cnambfre  37989  ftc1anclem5  38018  fzmul  38062  isismty  38122  heibor1  38131  heiborlem3  38134  hlatjcl  39813  hlatjcom  39814  hlatlej1  39821  hlrelat5N  39847  2lplnmN  40005  2llnmj  40006  2lplnmj  40068  syl3an12  42648  dvdsexpnn  42765  elmapresaunres2  43203  fzneg  43410  lsmfgcl  43502  trelded  44992  jaoded  44993  el123  45190  suctrALT  45252  suctrALTcf  45348  fnfocofob  47527  ltsubsubaddltsub  47749  fmtnoprmfac2lem1  48029  gboge9  48240  bgoldbtbndlem3  48283  usgrgrtrirex  48426  gpgedg2iv  48543  nnsgrp  48653  2zrngALT  48730  nn0sumltlt  48826  lincsum  48905  dignn0fr  49077  dignn0flhalflem2  49092