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  3569  euelss  4295  3elpr2eq  4870  funtpg  6571  fresaun  6731  fresaunres2  6732  ftpg  7128  eloprabga  7498  elmapresaun  8853  djuenun  10124  addasspi  10848  mulasspi  10850  distrpi  10851  addcanpi  10852  mulcanpi  10853  ltapi  10856  lemul1  12034  ltdiv2  12069  zletr  12577  zdivadd  12605  eluzsub  12823  nn01to3  12900  qdivcl  12929  maxle  13151  lemin  13152  maxlt  13153  ltmin  13154  xaddass  13209  xmulasslem3  13246  xadddilem  13254  iooneg  13432  zltaddlt1le  13466  fzen  13502  fzaddel  13519  fzadd2  13520  fzrev  13548  fzrevral2  13574  fzshftral  13576  fzosubel2  13686  fzonn0p1p1  13705  fldiv2  13823  modmulnn  13851  modcyc2  13869  prsshashgt1  14375  hashssdif  14377  pfxccatin12lem4  14691  fsum0diag2  15749  binomrisefac  16008  efsub  16068  dvdsnegb  16243  muldvds1  16250  muldvds2  16251  dvdscmul  16252  dvdsmulc  16253  dvdscmulr  16254  dvdsmulcr  16255  dvds2add  16260  dvds2sub  16261  dvdstr  16264  addmodlteqALT  16295  divalglem8  16370  divalgb  16374  divalgmod  16376  ndvdsadd  16380  modgcd  16502  absmulgcd  16519  rpmulgcd  16527  zexpgcd  16535  cncongr2  16638  hashdvds  16745  pythagtriplem1  16787  vdwlem3  16954  ressinbas  17215  gsumws2  18769  mulgmodid  19045  nmzsubg  19097  pmtr3ncomlem1  19403  pmtrdifellem1  19406  subcmn  19767  gexexlem  19782  lsmcom  19788  zaddablx  19802  gsumpr  19885  c0snghm  20373  isdomn4  20625  drngmcl  20659  psgnghm  21489  phlssphl  21568  assa2ass  21772  psrbagconf1o  21838  gsumbagdiaglem  21839  psrass1lem  21841  psrass1  21873  mplmonmul  21943  psdmul  22053  ply1opprmul  22123  coe1mul  22156  2ndcdisj2  23344  fbssfi  23724  isfcf  23921  nmotri  24627  nghmplusg  24628  0nmhm  24643  iundisj2  25450  ovolioo  25469  uniiccdif  25479  basellem9  26999  cplgr2vpr  29360  redwlk  29600  clwwlknccat  29992  frgrwopreglem5a  30240  lnocoi  30686  ipasslem5  30764  hhssabloilem  31190  hhssnv  31193  shscli  31246  shmodsi  31318  lnopmi  31929  lnopcoi  31932  cnlnadjlem2  31997  adjmul  32021  leopmul2i  32064  leoptr  32066  pjimai  32105  mdslle1i  32246  mdslle2i  32247  mdslj1i  32248  mdslj2i  32249  mdslmd1lem1  32254  mdslmd2i  32259  atexch  32310  atcvatlem  32314  chirredlem3  32321  sumdmdii  32344  sumdmdlem  32347  cdj3i  32370  iundisj2f  32519  iundisj2fi  32720  xrge0omnd  33025  srafldlvec  33582  bnj1384  35022  revpfxsfxrev  35103  satffunlem2lem1  35391  cgr3permute3  36035  cgr3permute1  36036  cgr3com  36041  nndivsub  36445  lindsadd  37607  mblfinlem2  37652  cnambfre  37662  ftc1anclem5  37691  fzmul  37735  isismty  37795  heibor1  37804  heiborlem3  37807  hlatjcl  39360  hlatjcom  39361  hlatlej1  39368  hlrelat5N  39395  2lplnmN  39553  2llnmj  39554  2lplnmj  39616  syl3an12  42197  dvdsexpnn  42321  elmapresaunres2  42759  fzneg  42971  lsmfgcl  43063  trelded  44555  jaoded  44556  el123  44753  suctrALT  44815  suctrALTcf  44911  fnfocofob  47080  ltsubsubaddltsub  47302  fmtnoprmfac2lem1  47567  gboge9  47765  bgoldbtbndlem3  47808  usgrgrtrirex  47949  gpgedg2iv  48058  nnsgrp  48165  2zrngALT  48242  nn0sumltlt  48338  lincsum  48418  dignn0fr  48590  dignn0flhalflem2  48605