Theorem syl3an 1166

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

Syntax hints:   → wi 4   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  syl2an3an  1430  spc3egv  3548  euelss  4267  3elpr2eq  4844  funtpg  6547  fresaun  6705  fresaunres2  6706  ftpg  7106  eloprabga  7472  elmapresaun  8825  djuenun  10091  addasspi  10816  mulasspi  10818  distrpi  10819  addcanpi  10820  mulcanpi  10821  ltapi  10824  lemul1  12005  ltdiv2  12040  zletr  12569  zdivadd  12598  eluzsub  12816  nn01to3  12889  qdivcl  12918  maxle  13141  lemin  13142  maxlt  13143  ltmin  13144  xaddass  13199  xmulasslem3  13236  xadddilem  13244  iooneg  13422  zltaddlt1le  13456  fzen  13493  fzaddel  13510  fzadd2  13511  fzrev  13539  fzrevral2  13565  fzshftral  13567  fzosubel2  13678  fzonn0p1p1  13697  fldiv2  13818  modmulnn  13846  modcyc2  13864  prsshashgt1  14370  hashssdif  14372  pfxccatin12lem4  14686  fsum0diag2  15743  binomrisefac  16005  efsub  16065  dvdsnegb  16240  muldvds1  16247  muldvds2  16248  dvdscmul  16249  dvdsmulc  16250  dvdscmulr  16251  dvdsmulcr  16252  dvds2add  16257  dvds2sub  16258  dvdstr  16261  addmodlteqALT  16292  divalglem8  16367  divalgb  16371  divalgmod  16373  ndvdsadd  16377  modgcd  16499  absmulgcd  16516  rpmulgcd  16524  zexpgcd  16532  cncongr2  16635  hashdvds  16743  pythagtriplem1  16785  vdwlem3  16952  ressinbas  17213  gsumws2  18808  mulgmodid  19087  nmzsubg  19138  pmtr3ncomlem1  19446  pmtrdifellem1  19449  subcmn  19810  gexexlem  19825  lsmcom  19831  zaddablx  19845  gsumpr  19928  c0snghm  20442  isdomn4  20695  drngmcl  20729  xrge0omnd  21427  psgnghm  21562  phlssphl  21641  assa2ass  21845  psrbagconf1o  21911  gsumbagdiaglem  21913  psrass1lem  21915  psrass1  21945  mplmonmul  22019  psdmul  22161  ply1opprmul  22230  coe1mul  22263  2ndcdisj2  23447  fbssfi  23827  isfcf  24024  nmotri  24729  nghmplusg  24730  0nmhm  24745  iundisj2  25541  ovolioo  25560  uniiccdif  25570  basellem9  27077  zsoring  28426  cplgr2vpr  29527  redwlk  29764  clwwlknccat  30158  frgrwopreglem5a  30406  lnocoi  30853  ipasslem5  30931  hhssabloilem  31357  hhssnv  31360  shscli  31413  shmodsi  31485  lnopmi  32096  lnopcoi  32099  cnlnadjlem2  32164  adjmul  32188  leopmul2i  32231  leoptr  32233  pjimai  32272  mdslle1i  32413  mdslle2i  32414  mdslj1i  32415  mdslj2i  32416  mdslmd1lem1  32421  mdslmd2i  32426  atexch  32477  atcvatlem  32481  chirredlem3  32488  sumdmdii  32511  sumdmdlem  32514  cdj3i  32537  iundisj2f  32686  iundisj2fi  32896  psrmonmul  33741  srafldlvec  33777  bnj1384  35221  revpfxsfxrev  35351  satffunlem2lem1  35639  cgr3permute3  36282  cgr3permute1  36283  cgr3com  36288  nndivsub  36692  lindsadd  37987  mblfinlem2  38032  cnambfre  38042  ftc1anclem5  38071  fzmul  38115  isismty  38175  heibor1  38184  heiborlem3  38187  hlatjcl  39866  hlatjcom  39867  hlatlej1  39874  hlrelat5N  39900  2lplnmN  40058  2llnmj  40059  2lplnmj  40121  syl3an12  42701  dvdsexpnn  42817  elmapresaunres2  43227  fzneg  43434  lsmfgcl  43526  trelded  45016  jaoded  45017  el123  45214  suctrALT  45276  suctrALTcf  45372  fnfocofob  47549  ltsubsubaddltsub  47771  fmtnoprmfac2lem1  48051  gboge9  48262  bgoldbtbndlem3  48305  usgrgrtrirex  48448  gpgedg2iv  48565  nnsgrp  48675  2zrngALT  48752  nn0sumltlt  48848  lincsum  48927  dignn0fr  49099  dignn0flhalflem2  49114