Theorem syl3an 1156

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

Syntax hints:   → wi 4   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  syl2an3an  1418  spc3egv  3607  euelss  4293  3elpr2eq  4840  funtpg  6412  fresaun  6552  fresaunres2  6553  ftpg  6921  eloprabga  7264  elmapresaun  8447  djuenun  9599  addasspi  10320  mulasspi  10322  distrpi  10323  addcanpi  10324  mulcanpi  10325  ltapi  10328  lemul1  11495  ltdiv2  11529  zletr  12029  zdivadd  12056  nn01to3  12344  qdivcl  12372  maxle  12587  lemin  12588  maxlt  12589  ltmin  12590  xaddass  12645  xmulasslem3  12682  xadddilem  12690  iooneg  12860  zltaddlt1le  12893  fzen  12927  fzaddel  12944  fzadd2  12945  fzrev  12973  fzrevral2  12996  fzshftral  12998  fzosubel2  13100  fzonn0p1p1  13119  fldiv2  13232  modmulnn  13260  modcyc2  13278  prsshashgt1  13774  hashssdif  13776  ccatw2s1assOLD  13993  pfxccatin12lem4  14091  fsum0diag2  15141  binomrisefac  15399  efsub  15456  dvdsnegb  15630  muldvds1  15637  muldvds2  15638  dvdscmul  15639  dvdsmulc  15640  dvdscmulr  15641  dvdsmulcr  15642  dvds2add  15646  dvds2sub  15647  dvdstr  15649  addmodlteqALT  15678  divalglem8  15754  divalgb  15758  divalgmod  15760  ndvdsadd  15764  modgcd  15883  absmulgcd  15900  rpmulgcd  15909  cncongr2  16015  hashdvds  16115  pythagtriplem1  16156  vdwlem3  16322  ressinbas  16563  gsumws2  18010  mulgmodid  18269  nmzsubg  18320  pmtr3ncomlem1  18604  pmtrdifellem1  18607  subcmn  18960  gexexlem  18975  lsmcom  18981  zaddablx  18995  gsumpr  19078  assa2ass  20098  psrbagconf1o  20157  gsumbagdiaglem  20158  psrass1lem  20160  psrass1  20188  mplmonmul  20248  ply1opprmul  20410  coe1mul  20441  psgnghm  20727  phlssphl  20806  2ndcdisj2  22068  fbssfi  22448  isfcf  22645  nmotri  23351  nghmplusg  23352  0nmhm  23367  iundisj2  24153  ovolioo  24172  uniiccdif  24182  basellem9  25669  cplgr2vpr  27218  redwlk  27457  clwwlknccat  27845  frgrwopreglem5a  28093  lnocoi  28537  ipasslem5  28615  hhssabloilem  29041  hhssnv  29044  shscli  29097  shmodsi  29169  lnopmi  29780  lnopcoi  29783  cnlnadjlem2  29848  adjmul  29872  leopmul2i  29915  leoptr  29917  pjimai  29956  mdslle1i  30097  mdslle2i  30098  mdslj1i  30099  mdslj2i  30100  mdslmd1lem1  30105  mdslmd2i  30110  atexch  30161  atcvatlem  30165  chirredlem3  30172  sumdmdii  30195  sumdmdlem  30198  cdj3i  30221  iundisj2f  30343  iundisj2fi  30523  xrge0omnd  30716  srafldlvec  30995  bnj1384  32308  revpfxsfxrev  32366  satffunlem2lem1  32655  noetalem5  33225  cgr3permute3  33512  cgr3permute1  33513  cgr3com  33518  nndivsub  33809  lindsadd  34889  mblfinlem2  34934  cnambfre  34944  ftc1anclem5  34975  fzmul  35020  isismty  35083  heibor1  35092  heiborlem3  35095  hlatjcl  36507  hlatjcom  36508  hlatlej1  36515  hlrelat5N  36541  2lplnmN  36699  2llnmj  36700  2lplnmj  36762  zexpgcd  39191  elmapresaunres2  39374  fzneg  39585  lsmfgcl  39680  trelded  40905  jaoded  40906  el123  41104  suctrALT  41166  suctrALTcf  41262  ltsubsubaddltsub  43508  fmtnoprmfac2lem1  43735  gboge9  43936  bgoldbtbndlem3  43979  nnsgrp  44091  c0snghm  44194  2zrngALT  44226  nn0sumltlt  44405  lincsum  44491  dignn0fr  44668  dignn0flhalflem2  44683