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  3560  euelss  4281  3elpr2eq  4869  funtpg  6592  fresaun  6750  fresaunres2  6751  ftpg  7157  eloprabga  7526  elmapresaun  8891  djuenun  10177  addasspi  10908  mulasspi  10910  distrpi  10911  addcanpi  10912  mulcanpi  10913  ltapi  10916  lemul1  12095  ltdiv2  12129  zletr  12666  zdivadd  12696  eluzsub  12921  nn01to3  12994  qdivcl  13024  maxle  13247  lemin  13248  maxlt  13249  ltmin  13250  xaddass  13305  xmulasslem3  13342  xadddilem  13350  iooneg  13528  zltaddlt1le  13562  fzen  13599  fzaddel  13617  fzadd2  13618  fzrev  13646  fzrevral2  13672  fzshftral  13674  fzosubel2  13785  fzonn0p1p1  13804  fldiv2  13926  modmulnn  13954  modcyc2  13972  prsshashgt1  14479  hashssdif  14481  pfxccatin12lem4  14799  revpfxsfxrev  14841  fsum0diag2  15873  binomrisefac  16134  efsub  16194  dvdsnegb  16369  muldvds1  16376  muldvds2  16377  dvdscmul  16378  dvdsmulc  16379  dvdscmulr  16380  dvdsmulcr  16381  dvds2add  16386  dvds2sub  16387  dvdstr  16390  addmodlteqALT  16421  divalglem8  16496  divalgb  16500  divalgmod  16502  ndvdsadd  16506  modgcd  16628  absmulgcd  16645  rpmulgcd  16653  zexpgcd  16661  cncongr2  16764  hashdvds  16872  pythagtriplem1  16914  vdwlem3  17081  ressinbas  17343  gsumws2  18957  mulgmodid  19242  nmzsubg  19294  pmtr3ncomlem1  19606  pmtrdifellem1  19609  subcmn  19970  gexexlem  19985  lsmcom  19991  zaddablx  20005  gsumpr  20088  c0snghm  20611  isdomn4  20883  isdrng3lem2  20921  drngmcl  20924  xrge0omnd  21664  psgnghm  21799  phlssphl  21878  assa2ass  22084  psrbagconf1o  22150  gsumbagdiaglem  22152  psrass1lem  22154  psrass1  22184  mplmonmul  22258  psdmul  22400  ply1opprmul  22469  coe1mul  22502  2ndcdisj2  23689  fbssfi  24069  isfcf  24266  nmotri  24971  nghmplusg  24972  0nmhm  24987  iundisj2  25783  ovolioo  25802  uniiccdif  25812  basellem9  27333  zsoring  28682  cplgr2vpr  29901  redwlk  30138  clwwlknccat  30541  frgrwopreglem5a  30799  lnocoi  31246  ipasslem5  31324  hhssabloilem  31750  hhssnv  31753  shscli  31806  shmodsi  31878  lnopmi  32489  lnopcoi  32492  cnlnadjlem2  32557  adjmul  32581  leopmul2i  32624  leoptr  32626  pjimai  32665  mdslle1i  32806  mdslle2i  32807  mdslj1i  32808  mdslj2i  32809  mdslmd1lem1  32814  mdslmd2i  32819  atexch  32870  atcvatlem  32874  chirredlem3  32881  sumdmdii  32904  sumdmdlem  32907  cdj3i  32930  iundisj2f  33071  iundisj2fi  33276  psrmonmul  34068  srafldlvec  34104  bnj1384  35549  satffunlem2lem1  35991  cgr3permute3  36635  cgr3permute1  36636  cgr3com  36641  nndivsub  37084  lindsadd  38375  mblfinlem2  38415  cnambfre  38425  ftc1anclem5  38454  fzmul  38499  isismty  38559  heibor1  38568  heiborlem3  38571  hlatjcl  40248  hlatjcom  40249  hlatlej1  40256  hlrelat5N  40282  2lplnmN  40440  2llnmj  40441  2lplnmj  40503  syl3an12  43085  dvdsexpnn  43216  elmapresaunres2  43624  fzneg  43831  lsmfgcl  43923  trelded  45396  jaoded  45397  el123  45594  suctrALT  45656  suctrALTcf  45752  fnfocofob  47975  ltsubsubaddltsub  48197  fmtnoprmfac2lem1  48477  gboge9  48688  bgoldbtbndlem3  48731  usgrgrtrirex  48874  gpgedg2iv  48991  nnsgrp  49100  2zrngALT  49177  nn0sumltlt  49288  lincsum  49367  dignn0fr  49539  dignn0flhalflem2  49554