Theorem syl3an 1159

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 1150	. 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  syl2an3an  1421  spc3egv  3543  euelss  4256  3elpr2eq  4839  funtpg  6496  fresaun  6654  fresaunres2  6655  ftpg  7037  eloprabga  7391  eloprabgaOLD  7392  elmapresaun  8677  djuenun  9935  addasspi  10660  mulasspi  10662  distrpi  10663  addcanpi  10664  mulcanpi  10665  ltapi  10668  lemul1  11836  ltdiv2  11870  zletr  12373  zdivadd  12400  nn01to3  12690  qdivcl  12719  maxle  12934  lemin  12935  maxlt  12936  ltmin  12937  xaddass  12992  xmulasslem3  13029  xadddilem  13037  iooneg  13212  zltaddlt1le  13246  fzen  13282  fzaddel  13299  fzadd2  13300  fzrev  13328  fzrevral2  13351  fzshftral  13353  fzosubel2  13456  fzonn0p1p1  13475  fldiv2  13590  modmulnn  13618  modcyc2  13636  prsshashgt1  14134  hashssdif  14136  ccatw2s1assOLD  14350  pfxccatin12lem4  14448  fsum0diag2  15504  binomrisefac  15761  efsub  15818  dvdsnegb  15992  muldvds1  15999  muldvds2  16000  dvdscmul  16001  dvdsmulc  16002  dvdscmulr  16003  dvdsmulcr  16004  dvds2add  16008  dvds2sub  16009  dvdstr  16012  addmodlteqALT  16043  divalglem8  16118  divalgb  16122  divalgmod  16124  ndvdsadd  16128  modgcd  16249  absmulgcd  16266  rpmulgcd  16275  cncongr2  16382  hashdvds  16485  pythagtriplem1  16526  vdwlem3  16693  ressinbas  16964  gsumws2  18490  mulgmodid  18751  nmzsubg  18802  pmtr3ncomlem1  19090  pmtrdifellem1  19093  subcmn  19447  gexexlem  19462  lsmcom  19468  zaddablx  19482  gsumpr  19565  psgnghm  20794  phlssphl  20873  assa2ass  21079  psrbagconf1o  21148  psrbagconf1oOLD  21149  gsumbagdiaglemOLD  21150  psrass1lemOLD  21152  gsumbagdiaglem  21153  psrass1lem  21155  psrass1  21183  mplmonmul  21246  ply1opprmul  21419  coe1mul  21450  2ndcdisj2  22617  fbssfi  22997  isfcf  23194  nmotri  23912  nghmplusg  23913  0nmhm  23928  iundisj2  24722  ovolioo  24741  uniiccdif  24751  basellem9  26247  cplgr2vpr  27809  redwlk  28049  clwwlknccat  28436  frgrwopreglem5a  28684  lnocoi  29128  ipasslem5  29206  hhssabloilem  29632  hhssnv  29635  shscli  29688  shmodsi  29760  lnopmi  30371  lnopcoi  30374  cnlnadjlem2  30439  adjmul  30463  leopmul2i  30506  leoptr  30508  pjimai  30547  mdslle1i  30688  mdslle2i  30689  mdslj1i  30690  mdslj2i  30691  mdslmd1lem1  30696  mdslmd2i  30701  atexch  30752  atcvatlem  30756  chirredlem3  30763  sumdmdii  30786  sumdmdlem  30789  cdj3i  30812  iundisj2f  30938  iundisj2fi  31127  xrge0omnd  31346  srafldlvec  31685  bnj1384  33021  revpfxsfxrev  33086  satffunlem2lem1  33375  cgr3permute3  34358  cgr3permute1  34359  cgr3com  34364  nndivsub  34655  lindsadd  35779  mblfinlem2  35824  cnambfre  35834  ftc1anclem5  35863  fzmul  35908  isismty  35968  heibor1  35977  heiborlem3  35980  hlatjcl  37388  hlatjcom  37389  hlatlej1  37396  hlrelat5N  37422  2lplnmN  37580  2llnmj  37581  2lplnmj  37643  factwoffsmonot  40170  isdomn4  40179  syl3an12  40182  zexpgcd  40343  dvdsexpnn  40347  elmapresaunres2  40600  fzneg  40811  lsmfgcl  40906  trelded  42192  jaoded  42193  el123  42391  suctrALT  42453  suctrALTcf  42549  fnfocofob  44582  ltsubsubaddltsub  44804  fmtnoprmfac2lem1  45029  gboge9  45227  bgoldbtbndlem3  45270  nnsgrp  45382  c0snghm  45485  2zrngALT  45517  nn0sumltlt  45697  lincsum  45781  dignn0fr  45958  dignn0flhalflem2  45973