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  3558  euelss  4282  3elpr2eq  4858  funtpg  6536  fresaun  6694  fresaunres2  6695  ftpg  7089  eloprabga  7455  elmapresaun  8804  djuenun  10059  addasspi  10783  mulasspi  10785  distrpi  10786  addcanpi  10787  mulcanpi  10788  ltapi  10791  lemul1  11970  ltdiv2  12005  zletr  12513  zdivadd  12541  eluzsub  12759  nn01to3  12836  qdivcl  12865  maxle  13087  lemin  13088  maxlt  13089  ltmin  13090  xaddass  13145  xmulasslem3  13182  xadddilem  13190  iooneg  13368  zltaddlt1le  13402  fzen  13438  fzaddel  13455  fzadd2  13456  fzrev  13484  fzrevral2  13510  fzshftral  13512  fzosubel2  13622  fzonn0p1p1  13641  fldiv2  13762  modmulnn  13790  modcyc2  13808  prsshashgt1  14314  hashssdif  14316  pfxccatin12lem4  14630  fsum0diag2  15687  binomrisefac  15946  efsub  16006  dvdsnegb  16181  muldvds1  16188  muldvds2  16189  dvdscmul  16190  dvdsmulc  16191  dvdscmulr  16192  dvdsmulcr  16193  dvds2add  16198  dvds2sub  16199  dvdstr  16202  addmodlteqALT  16233  divalglem8  16308  divalgb  16312  divalgmod  16314  ndvdsadd  16318  modgcd  16440  absmulgcd  16457  rpmulgcd  16465  zexpgcd  16473  cncongr2  16576  hashdvds  16683  pythagtriplem1  16725  vdwlem3  16892  ressinbas  17153  gsumws2  18747  mulgmodid  19023  nmzsubg  19075  pmtr3ncomlem1  19383  pmtrdifellem1  19386  subcmn  19747  gexexlem  19762  lsmcom  19768  zaddablx  19782  gsumpr  19865  c0snghm  20380  isdomn4  20629  drngmcl  20663  xrge0omnd  21380  psgnghm  21515  phlssphl  21594  assa2ass  21798  psrbagconf1o  21864  gsumbagdiaglem  21865  psrass1lem  21867  psrass1  21899  mplmonmul  21969  psdmul  22079  ply1opprmul  22149  coe1mul  22182  2ndcdisj2  23370  fbssfi  23750  isfcf  23947  nmotri  24652  nghmplusg  24653  0nmhm  24668  iundisj2  25475  ovolioo  25494  uniiccdif  25504  basellem9  27024  zsoring  28330  cplgr2vpr  29409  redwlk  29647  clwwlknccat  30038  frgrwopreglem5a  30286  lnocoi  30732  ipasslem5  30810  hhssabloilem  31236  hhssnv  31239  shscli  31292  shmodsi  31364  lnopmi  31975  lnopcoi  31978  cnlnadjlem2  32043  adjmul  32067  leopmul2i  32110  leoptr  32112  pjimai  32151  mdslle1i  32292  mdslle2i  32293  mdslj1i  32294  mdslj2i  32295  mdslmd1lem1  32300  mdslmd2i  32305  atexch  32356  atcvatlem  32360  chirredlem3  32367  sumdmdii  32390  sumdmdlem  32393  cdj3i  32416  iundisj2f  32565  iundisj2fi  32774  srafldlvec  33593  bnj1384  35039  revpfxsfxrev  35148  satffunlem2lem1  35436  cgr3permute3  36080  cgr3permute1  36081  cgr3com  36086  nndivsub  36490  lindsadd  37652  mblfinlem2  37697  cnambfre  37707  ftc1anclem5  37736  fzmul  37780  isismty  37840  heibor1  37849  heiborlem3  37852  hlatjcl  39405  hlatjcom  39406  hlatlej1  39413  hlrelat5N  39439  2lplnmN  39597  2llnmj  39598  2lplnmj  39660  syl3an12  42241  dvdsexpnn  42365  elmapresaunres2  42803  fzneg  43014  lsmfgcl  43106  trelded  44597  jaoded  44598  el123  44795  suctrALT  44857  suctrALTcf  44953  fnfocofob  47109  ltsubsubaddltsub  47331  fmtnoprmfac2lem1  47596  gboge9  47794  bgoldbtbndlem3  47837  usgrgrtrirex  47980  gpgedg2iv  48097  nnsgrp  48207  2zrngALT  48284  nn0sumltlt  48380  lincsum  48460  dignn0fr  48632  dignn0flhalflem2  48647