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  3572  euelss  4298  3elpr2eq  4873  funtpg  6574  fresaun  6734  fresaunres2  6735  ftpg  7131  eloprabga  7501  elmapresaun  8856  djuenun  10131  addasspi  10855  mulasspi  10857  distrpi  10858  addcanpi  10859  mulcanpi  10860  ltapi  10863  lemul1  12041  ltdiv2  12076  zletr  12584  zdivadd  12612  eluzsub  12830  nn01to3  12907  qdivcl  12936  maxle  13158  lemin  13159  maxlt  13160  ltmin  13161  xaddass  13216  xmulasslem3  13253  xadddilem  13261  iooneg  13439  zltaddlt1le  13473  fzen  13509  fzaddel  13526  fzadd2  13527  fzrev  13555  fzrevral2  13581  fzshftral  13583  fzosubel2  13693  fzonn0p1p1  13712  fldiv2  13830  modmulnn  13858  modcyc2  13876  prsshashgt1  14382  hashssdif  14384  pfxccatin12lem4  14698  fsum0diag2  15756  binomrisefac  16015  efsub  16075  dvdsnegb  16250  muldvds1  16257  muldvds2  16258  dvdscmul  16259  dvdsmulc  16260  dvdscmulr  16261  dvdsmulcr  16262  dvds2add  16267  dvds2sub  16268  dvdstr  16271  addmodlteqALT  16302  divalglem8  16377  divalgb  16381  divalgmod  16383  ndvdsadd  16387  modgcd  16509  absmulgcd  16526  rpmulgcd  16534  zexpgcd  16542  cncongr2  16645  hashdvds  16752  pythagtriplem1  16794  vdwlem3  16961  ressinbas  17222  gsumws2  18776  mulgmodid  19052  nmzsubg  19104  pmtr3ncomlem1  19410  pmtrdifellem1  19413  subcmn  19774  gexexlem  19789  lsmcom  19795  zaddablx  19809  gsumpr  19892  c0snghm  20380  isdomn4  20632  drngmcl  20666  psgnghm  21496  phlssphl  21575  assa2ass  21779  psrbagconf1o  21845  gsumbagdiaglem  21846  psrass1lem  21848  psrass1  21880  mplmonmul  21950  psdmul  22060  ply1opprmul  22130  coe1mul  22163  2ndcdisj2  23351  fbssfi  23731  isfcf  23928  nmotri  24634  nghmplusg  24635  0nmhm  24650  iundisj2  25457  ovolioo  25476  uniiccdif  25486  basellem9  27006  cplgr2vpr  29367  redwlk  29607  clwwlknccat  29999  frgrwopreglem5a  30247  lnocoi  30693  ipasslem5  30771  hhssabloilem  31197  hhssnv  31200  shscli  31253  shmodsi  31325  lnopmi  31936  lnopcoi  31939  cnlnadjlem2  32004  adjmul  32028  leopmul2i  32071  leoptr  32073  pjimai  32112  mdslle1i  32253  mdslle2i  32254  mdslj1i  32255  mdslj2i  32256  mdslmd1lem1  32261  mdslmd2i  32266  atexch  32317  atcvatlem  32321  chirredlem3  32328  sumdmdii  32351  sumdmdlem  32354  cdj3i  32377  iundisj2f  32526  iundisj2fi  32727  xrge0omnd  33032  srafldlvec  33589  bnj1384  35029  revpfxsfxrev  35110  satffunlem2lem1  35398  cgr3permute3  36042  cgr3permute1  36043  cgr3com  36048  nndivsub  36452  lindsadd  37614  mblfinlem2  37659  cnambfre  37669  ftc1anclem5  37698  fzmul  37742  isismty  37802  heibor1  37811  heiborlem3  37814  hlatjcl  39367  hlatjcom  39368  hlatlej1  39375  hlrelat5N  39402  2lplnmN  39560  2llnmj  39561  2lplnmj  39623  syl3an12  42204  dvdsexpnn  42328  elmapresaunres2  42766  fzneg  42978  lsmfgcl  43070  trelded  44562  jaoded  44563  el123  44760  suctrALT  44822  suctrALTcf  44918  fnfocofob  47084  ltsubsubaddltsub  47306  fmtnoprmfac2lem1  47571  gboge9  47769  bgoldbtbndlem3  47812  usgrgrtrirex  47953  gpgedg2iv  48062  nnsgrp  48169  2zrngALT  48246  nn0sumltlt  48342  lincsum  48422  dignn0fr  48594  dignn0flhalflem2  48609