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  1450  3jaao  1461  spc3egv  3561  euelss  4280  3elpr2eq  4837  funtpg  6617  fresaun  6775  fresaunres2  6776  ftpg  7184  eloprabga  7552  elmapresaun  8936  djuenun  10276  addasspi  11007  mulasspi  11009  distrpi  11010  addcanpi  11011  mulcanpi  11012  ltapi  11015  lemul1  12196  ltdiv2  12230  zletr  12767  zdivadd  12797  eluzsub  13022  nn01to3  13095  qdivcl  13125  maxle  13348  lemin  13349  maxlt  13350  ltmin  13351  xaddass  13406  xmulasslem3  13443  xadddilem  13451  iooneg  13629  zltaddlt1le  13663  fzen  13701  fzaddel  13719  fzadd2  13720  fzrev  13748  fzrevral2  13774  fzshftral  13776  fzosubel2  13887  fzonn0p1p1  13906  fldiv2  14028  modmulnn  14056  modcyc2  14074  prsshashgt1  14582  hashssdif  14584  pfxccatin12lem4  14903  revpfxsfxrev  14945  fsum0diag2  15978  binomrisefac  16237  efsub  16297  dvdsnegb  16472  muldvds1  16479  muldvds2  16480  dvdscmul  16481  dvdsmulc  16482  dvdscmulr  16483  dvdsmulcr  16484  dvds2add  16489  dvds2sub  16490  dvdstr  16493  addmodlteqALT  16524  divalglem8  16599  divalgb  16603  divalgmod  16605  ndvdsadd  16609  modgcd  16734  absmulgcd  16751  rpmulgcd  16760  zexpgcd  16768  dvdsexpnn  16769  cncongr2  16872  hashdvds  16981  pythagtriplem1  17023  vdwlem3  17190  ressinbas  17452  gsumws2  19067  mulgmodid  19352  nmzsubg  19404  pmtr3ncomlem1  19717  pmtrdifellem1  19720  subcmn  20081  gexexlem  20096  lsmcom  20102  zaddablx  20116  gsumpr  20199  c0snghm  20724  isdomn4  20997  isdrng3lem2  21036  drngmcl  21039  xrge0omnd  21781  psgnghm  21916  phlssphl  21995  assa2ass  22201  psrbagconf1o  22267  gsumbagdiaglem  22269  psrass1lem  22271  psrass1  22301  mplmonmul  22375  psdmul  22517  ply1opprmul  22586  coe1mul  22619  2ndcdisj2  23806  fbssfi  24186  isfcf  24383  nmotri  25088  nghmplusg  25089  0nmhm  25104  iundisj2  25900  ovolioo  25919  uniiccdif  25929  basellem9  27446  zsoring  28825  cplgr2vpr  30044  redwlk  30281  clwwlknccat  30684  frgrwopreglem5a  30942  lnocoi  31389  ipasslem5  31467  hhssabloilem  31893  hhssnv  31896  shscli  31949  shmodsi  32021  lnopmi  32632  lnopcoi  32635  cnlnadjlem2  32700  adjmul  32724  leopmul2i  32767  leoptr  32769  pjimai  32808  mdslle1i  32949  mdslle2i  32950  mdslj1i  32951  mdslj2i  32952  mdslmd1lem1  32957  mdslmd2i  32962  atexch  33013  atcvatlem  33017  chirredlem3  33024  sumdmdii  33047  sumdmdlem  33050  cdj3i  33073  iundisj2f  33256  iundisj2fi  33459  psrmonmul  34252  srafldlvec  34288  bnj1384  35732  satffunlem2lem1  36336  cgr3permute3  36990  cgr3permute1  36991  cgr3com  36996  nndivsub  37423  lindsadd  38728  mblfinlem2  38768  cnambfre  38778  ftc1anclem5  38807  fzmul  38867  isismty  38927  heibor1  38936  heiborlem3  38939  hlatjcl  40616  hlatjcom  40617  hlatlej1  40624  hlrelat5N  40650  2lplnmN  40808  2llnmj  40809  2lplnmj  40871  syl3an12  43453  elmapresaunres2  43975  fzneg  44182  lsmfgcl  44269  trelded  45739  jaoded  45740  el123  45937  suctrALT  45999  suctrALTcf  46095  fnfocofob  48354  ltsubsubaddltsub  48576  fmtnoprmfac2lem1  48856  gboge9  49067  bgoldbtbndlem3  49110  usgrgrtrirex  49253  gpgedg2iv  49370  nnsgrp  49479  2zrngALT  49556  nn0sumltlt  49667  lincsum  49746  dignn0fr  49918  dignn0flhalflem2  49933