Theorem syl3an 1178

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

Syntax hints:   → wi 4   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  syl2an3an  1449  3jaao  1460  spc3egv  3563  euelss  4286  3elpr2eq  4872  funtpg  6593  fresaun  6751  fresaunres2  6752  ftpg  7155  eloprabga  7521  elmapresaun  8879  djuenun  10155  addasspi  10881  mulasspi  10883  distrpi  10884  addcanpi  10885  mulcanpi  10886  ltapi  10889  lemul1  12068  ltdiv2  12102  zletr  12639  zdivadd  12668  eluzsub  12893  nn01to3  12966  qdivcl  12995  maxle  13218  lemin  13219  maxlt  13220  ltmin  13221  xaddass  13276  xmulasslem3  13313  xadddilem  13321  iooneg  13499  zltaddlt1le  13533  fzen  13570  fzaddel  13588  fzadd2  13589  fzrev  13617  fzrevral2  13643  fzshftral  13645  fzosubel2  13756  fzonn0p1p1  13775  fldiv2  13896  modmulnn  13924  modcyc2  13942  prsshashgt1  14449  hashssdif  14451  pfxccatin12lem4  14765  fsum0diag2  15836  binomrisefac  16097  efsub  16157  dvdsnegb  16332  muldvds1  16339  muldvds2  16340  dvdscmul  16341  dvdsmulc  16342  dvdscmulr  16343  dvdsmulcr  16344  dvds2add  16349  dvds2sub  16350  dvdstr  16353  addmodlteqALT  16384  divalglem8  16459  divalgb  16463  divalgmod  16465  ndvdsadd  16469  modgcd  16591  absmulgcd  16608  rpmulgcd  16616  zexpgcd  16624  cncongr2  16727  hashdvds  16835  pythagtriplem1  16877  vdwlem3  17044  ressinbas  17306  gsumws2  18902  mulgmodid  19180  nmzsubg  19232  pmtr3ncomlem1  19544  pmtrdifellem1  19547  subcmn  19908  gexexlem  19923  lsmcom  19929  zaddablx  19943  gsumpr  20026  c0snghm  20547  isdomn4  20801  drngmcl  20837  xrge0omnd  21576  psgnghm  21711  phlssphl  21790  assa2ass  21994  psrbagconf1o  22060  gsumbagdiaglem  22062  psrass1lem  22064  psrass1  22094  mplmonmul  22168  psdmul  22310  ply1opprmul  22379  coe1mul  22412  2ndcdisj2  23595  fbssfi  23975  isfcf  24172  nmotri  24877  nghmplusg  24878  0nmhm  24893  iundisj2  25689  ovolioo  25708  uniiccdif  25718  basellem9  27231  zsoring  28580  cplgr2vpr  29761  redwlk  29998  clwwlknccat  30392  frgrwopreglem5a  30640  lnocoi  31087  ipasslem5  31165  hhssabloilem  31591  hhssnv  31594  shscli  31647  shmodsi  31719  lnopmi  32330  lnopcoi  32333  cnlnadjlem2  32398  adjmul  32422  leopmul2i  32465  leoptr  32467  pjimai  32506  mdslle1i  32647  mdslle2i  32648  mdslj1i  32649  mdslj2i  32650  mdslmd1lem1  32655  mdslmd2i  32660  atexch  32711  atcvatlem  32715  chirredlem3  32722  sumdmdii  32745  sumdmdlem  32748  cdj3i  32771  iundisj2f  32913  iundisj2fi  33120  psrmonmul  33918  srafldlvec  33954  bnj1384  35398  revpfxsfxrev  35585  satffunlem2lem1  35874  cgr3permute3  36517  cgr3permute1  36518  cgr3com  36523  nndivsub  36946  lindsadd  38242  mblfinlem2  38287  cnambfre  38297  ftc1anclem5  38326  fzmul  38370  isismty  38430  heibor1  38439  heiborlem3  38442  hlatjcl  40119  hlatjcom  40120  hlatlej1  40127  hlrelat5N  40153  2lplnmN  40311  2llnmj  40312  2lplnmj  40374  syl3an12  42956  dvdsexpnn  43072  elmapresaunres2  43482  fzneg  43689  lsmfgcl  43781  trelded  45254  jaoded  45255  el123  45452  suctrALT  45514  suctrALTcf  45610  fnfocofob  47793  ltsubsubaddltsub  48015  fmtnoprmfac2lem1  48295  gboge9  48506  bgoldbtbndlem3  48549  usgrgrtrirex  48692  gpgedg2iv  48809  nnsgrp  48919  2zrngALT  48996  nn0sumltlt  49107  lincsum  49186  dignn0fr  49358  dignn0flhalflem2  49373