Theorem syl3an 1167

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

Syntax hints:   → wi 4   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  syl2an3an  1431  spc3egv  3542  euelss  4262  3elpr2eq  4839  funtpg  6543  fresaun  6701  fresaunres2  6702  ftpg  7102  eloprabga  7468  elmapresaun  8822  djuenun  10088  addasspi  10814  mulasspi  10816  distrpi  10817  addcanpi  10818  mulcanpi  10819  ltapi  10822  lemul1  12002  ltdiv2  12037  zletr  12566  zdivadd  12595  eluzsub  12813  nn01to3  12886  qdivcl  12915  maxle  13138  lemin  13139  maxlt  13140  ltmin  13141  xaddass  13196  xmulasslem3  13233  xadddilem  13241  iooneg  13419  zltaddlt1le  13453  fzen  13490  fzaddel  13507  fzadd2  13508  fzrev  13536  fzrevral2  13562  fzshftral  13564  fzosubel2  13675  fzonn0p1p1  13694  fldiv2  13815  modmulnn  13843  modcyc2  13861  prsshashgt1  14367  hashssdif  14369  pfxccatin12lem4  14683  fsum0diag2  15740  binomrisefac  16002  efsub  16062  dvdsnegb  16237  muldvds1  16244  muldvds2  16245  dvdscmul  16246  dvdsmulc  16247  dvdscmulr  16248  dvdsmulcr  16249  dvds2add  16254  dvds2sub  16255  dvdstr  16258  addmodlteqALT  16289  divalglem8  16364  divalgb  16368  divalgmod  16370  ndvdsadd  16374  modgcd  16496  absmulgcd  16513  rpmulgcd  16521  zexpgcd  16529  cncongr2  16632  hashdvds  16740  pythagtriplem1  16782  vdwlem3  16949  ressinbas  17210  gsumws2  18805  mulgmodid  19084  nmzsubg  19135  pmtr3ncomlem1  19442  pmtrdifellem1  19445  subcmn  19806  gexexlem  19821  lsmcom  19827  zaddablx  19841  gsumpr  19924  c0snghm  20438  isdomn4  20691  drngmcl  20725  xrge0omnd  21423  psgnghm  21558  phlssphl  21637  assa2ass  21841  psrbagconf1o  21907  gsumbagdiaglem  21909  psrass1lem  21911  psrass1  21941  mplmonmul  22015  psdmul  22157  ply1opprmul  22226  coe1mul  22259  2ndcdisj2  23443  fbssfi  23823  isfcf  24020  nmotri  24725  nghmplusg  24726  0nmhm  24741  iundisj2  25537  ovolioo  25556  uniiccdif  25566  basellem9  27073  zsoring  28421  cplgr2vpr  29522  redwlk  29759  clwwlknccat  30153  frgrwopreglem5a  30401  lnocoi  30848  ipasslem5  30926  hhssabloilem  31352  hhssnv  31355  shscli  31408  shmodsi  31480  lnopmi  32091  lnopcoi  32094  cnlnadjlem2  32159  adjmul  32183  leopmul2i  32226  leoptr  32228  pjimai  32267  mdslle1i  32408  mdslle2i  32409  mdslj1i  32410  mdslj2i  32411  mdslmd1lem1  32416  mdslmd2i  32421  atexch  32472  atcvatlem  32476  chirredlem3  32483  sumdmdii  32506  sumdmdlem  32509  cdj3i  32532  iundisj2f  32681  iundisj2fi  32891  psrmonmul  33744  srafldlvec  33780  bnj1384  35227  revpfxsfxrev  35357  satffunlem2lem1  35645  cgr3permute3  36288  cgr3permute1  36289  cgr3com  36294  nndivsub  36698  lindsadd  37993  mblfinlem2  38038  cnambfre  38048  ftc1anclem5  38077  fzmul  38121  isismty  38181  heibor1  38190  heiborlem3  38193  hlatjcl  39872  hlatjcom  39873  hlatlej1  39880  hlrelat5N  39906  2lplnmN  40064  2llnmj  40065  2lplnmj  40127  syl3an12  42707  dvdsexpnn  42823  elmapresaunres2  43233  fzneg  43440  lsmfgcl  43532  trelded  45022  jaoded  45023  el123  45220  suctrALT  45282  suctrALTcf  45378  fnfocofob  47554  ltsubsubaddltsub  47776  fmtnoprmfac2lem1  48056  gboge9  48267  bgoldbtbndlem3  48310  usgrgrtrirex  48453  gpgedg2iv  48570  nnsgrp  48680  2zrngALT  48757  nn0sumltlt  48853  lincsum  48932  dignn0fr  49104  dignn0flhalflem2  49119