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 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  syl2an3an  1449  3jaao  1460  spc3egv  3558  euelss  4278  3elpr2eq  4866  funtpg  6587  fresaun  6745  fresaunres2  6746  ftpg  7152  eloprabga  7521  elmapresaun  8892  djuenun  10230  addasspi  10961  mulasspi  10963  distrpi  10964  addcanpi  10965  mulcanpi  10966  ltapi  10969  lemul1  12150  ltdiv2  12184  zletr  12721  zdivadd  12751  eluzsub  12976  nn01to3  13049  qdivcl  13079  maxle  13302  lemin  13303  maxlt  13304  ltmin  13305  xaddass  13360  xmulasslem3  13397  xadddilem  13405  iooneg  13583  zltaddlt1le  13617  fzen  13654  fzaddel  13672  fzadd2  13673  fzrev  13701  fzrevral2  13727  fzshftral  13729  fzosubel2  13840  fzonn0p1p1  13859  fldiv2  13981  modmulnn  14009  modcyc2  14027  prsshashgt1  14535  hashssdif  14537  pfxccatin12lem4  14855  revpfxsfxrev  14897  fsum0diag2  15929  binomrisefac  16188  efsub  16248  dvdsnegb  16423  muldvds1  16430  muldvds2  16431  dvdscmul  16432  dvdsmulc  16433  dvdscmulr  16434  dvdsmulcr  16435  dvds2add  16440  dvds2sub  16441  dvdstr  16444  addmodlteqALT  16475  divalglem8  16550  divalgb  16554  divalgmod  16556  ndvdsadd  16560  modgcd  16685  absmulgcd  16702  rpmulgcd  16711  zexpgcd  16719  dvdsexpnn  16720  cncongr2  16823  hashdvds  16932  pythagtriplem1  16974  vdwlem3  17141  ressinbas  17403  gsumws2  19018  mulgmodid  19303  nmzsubg  19355  pmtr3ncomlem1  19667  pmtrdifellem1  19670  subcmn  20031  gexexlem  20046  lsmcom  20052  zaddablx  20066  gsumpr  20149  c0snghm  20674  isdomn4  20947  isdrng3lem2  20986  drngmcl  20989  xrge0omnd  21731  psgnghm  21866  phlssphl  21945  assa2ass  22151  psrbagconf1o  22217  gsumbagdiaglem  22219  psrass1lem  22221  psrass1  22251  mplmonmul  22325  psdmul  22467  ply1opprmul  22536  coe1mul  22569  2ndcdisj2  23756  fbssfi  24136  isfcf  24333  nmotri  25038  nghmplusg  25039  0nmhm  25054  iundisj2  25850  ovolioo  25869  uniiccdif  25879  basellem9  27398  zsoring  28777  cplgr2vpr  29996  redwlk  30233  clwwlknccat  30636  frgrwopreglem5a  30894  lnocoi  31341  ipasslem5  31419  hhssabloilem  31845  hhssnv  31848  shscli  31901  shmodsi  31973  lnopmi  32584  lnopcoi  32587  cnlnadjlem2  32652  adjmul  32676  leopmul2i  32719  leoptr  32721  pjimai  32760  mdslle1i  32901  mdslle2i  32902  mdslj1i  32903  mdslj2i  32904  mdslmd1lem1  32909  mdslmd2i  32914  atexch  32965  atcvatlem  32969  chirredlem3  32976  sumdmdii  32999  sumdmdlem  33002  cdj3i  33025  iundisj2f  33166  iundisj2fi  33371  psrmonmul  34164  srafldlvec  34200  bnj1384  35645  satffunlem2lem1  36138  cgr3permute3  36782  cgr3permute1  36783  cgr3com  36788  nndivsub  37215  lindsadd  38504  mblfinlem2  38544  cnambfre  38554  ftc1anclem5  38583  fzmul  38643  isismty  38703  heibor1  38712  heiborlem3  38715  hlatjcl  40392  hlatjcom  40393  hlatlej1  40400  hlrelat5N  40426  2lplnmN  40584  2llnmj  40585  2lplnmj  40647  syl3an12  43229  elmapresaunres2  43735  fzneg  43942  lsmfgcl  44034  trelded  45507  jaoded  45508  el123  45705  suctrALT  45767  suctrALTcf  45863  fnfocofob  48093  ltsubsubaddltsub  48315  fmtnoprmfac2lem1  48595  gboge9  48806  bgoldbtbndlem3  48849  usgrgrtrirex  48992  gpgedg2iv  49109  nnsgrp  49218  2zrngALT  49295  nn0sumltlt  49406  lincsum  49485  dignn0fr  49657  dignn0flhalflem2  49672