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  3546  euelss  4273  3elpr2eq  4850  funtpg  6547  fresaun  6705  fresaunres2  6706  ftpg  7103  eloprabga  7469  elmapresaun  8821  djuenun  10084  addasspi  10809  mulasspi  10811  distrpi  10812  addcanpi  10813  mulcanpi  10814  ltapi  10817  lemul1  11998  ltdiv2  12033  zletr  12562  zdivadd  12591  eluzsub  12809  nn01to3  12882  qdivcl  12911  maxle  13134  lemin  13135  maxlt  13136  ltmin  13137  xaddass  13192  xmulasslem3  13229  xadddilem  13237  iooneg  13415  zltaddlt1le  13449  fzen  13486  fzaddel  13503  fzadd2  13504  fzrev  13532  fzrevral2  13558  fzshftral  13560  fzosubel2  13671  fzonn0p1p1  13690  fldiv2  13811  modmulnn  13839  modcyc2  13857  prsshashgt1  14363  hashssdif  14365  pfxccatin12lem4  14679  fsum0diag2  15736  binomrisefac  15998  efsub  16058  dvdsnegb  16233  muldvds1  16240  muldvds2  16241  dvdscmul  16242  dvdsmulc  16243  dvdscmulr  16244  dvdsmulcr  16245  dvds2add  16250  dvds2sub  16251  dvdstr  16254  addmodlteqALT  16285  divalglem8  16360  divalgb  16364  divalgmod  16366  ndvdsadd  16370  modgcd  16492  absmulgcd  16509  rpmulgcd  16517  zexpgcd  16525  cncongr2  16628  hashdvds  16736  pythagtriplem1  16778  vdwlem3  16945  ressinbas  17206  gsumws2  18801  mulgmodid  19080  nmzsubg  19131  pmtr3ncomlem1  19439  pmtrdifellem1  19442  subcmn  19803  gexexlem  19818  lsmcom  19824  zaddablx  19838  gsumpr  19921  c0snghm  20435  isdomn4  20684  drngmcl  20718  xrge0omnd  21435  psgnghm  21570  phlssphl  21649  assa2ass  21853  psrbagconf1o  21919  gsumbagdiaglem  21920  psrass1lem  21922  psrass1  21952  mplmonmul  22024  psdmul  22142  ply1opprmul  22212  coe1mul  22245  2ndcdisj2  23432  fbssfi  23812  isfcf  24009  nmotri  24714  nghmplusg  24715  0nmhm  24730  iundisj2  25526  ovolioo  25545  uniiccdif  25555  basellem9  27066  zsoring  28415  cplgr2vpr  29516  redwlk  29754  clwwlknccat  30148  frgrwopreglem5a  30396  lnocoi  30843  ipasslem5  30921  hhssabloilem  31347  hhssnv  31350  shscli  31403  shmodsi  31475  lnopmi  32086  lnopcoi  32089  cnlnadjlem2  32154  adjmul  32178  leopmul2i  32221  leoptr  32223  pjimai  32262  mdslle1i  32403  mdslle2i  32404  mdslj1i  32405  mdslj2i  32406  mdslmd1lem1  32411  mdslmd2i  32416  atexch  32467  atcvatlem  32471  chirredlem3  32478  sumdmdii  32501  sumdmdlem  32504  cdj3i  32527  iundisj2f  32675  iundisj2fi  32885  psrmonmul  33709  srafldlvec  33745  bnj1384  35190  revpfxsfxrev  35314  satffunlem2lem1  35602  cgr3permute3  36245  cgr3permute1  36246  cgr3com  36251  nndivsub  36655  lindsadd  37948  mblfinlem2  37993  cnambfre  38003  ftc1anclem5  38032  fzmul  38076  isismty  38136  heibor1  38145  heiborlem3  38148  hlatjcl  39827  hlatjcom  39828  hlatlej1  39835  hlrelat5N  39861  2lplnmN  40019  2llnmj  40020  2lplnmj  40082  syl3an12  42662  dvdsexpnn  42779  elmapresaunres2  43217  fzneg  43428  lsmfgcl  43520  trelded  45010  jaoded  45011  el123  45208  suctrALT  45270  suctrALTcf  45366  fnfocofob  47539  ltsubsubaddltsub  47761  fmtnoprmfac2lem1  48041  gboge9  48252  bgoldbtbndlem3  48295  usgrgrtrirex  48438  gpgedg2iv  48555  nnsgrp  48665  2zrngALT  48742  nn0sumltlt  48838  lincsum  48917  dignn0fr  49089  dignn0flhalflem2  49104