Theorem syl3an 1320

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl2an3an  1339  funtpg  5432  ftpg  5899  eloprabga  6175  prfidisj  7234  djuenun  7569  addasspig  7698  mulasspig  7700  distrpig  7701  addcanpig  7702  mulcanpig  7703  ltapig  7706  distrnqg  7755  distrnq0  7827  cnegexlem2  8504  zletr  9699  zdivadd  9740  xaddass  10282  iooneg  10401  zltaddlt1le  10421  fzen  10458  fzaddel  10476  fzrev  10502  fzrevral2  10524  fzshftral  10526  fzosubel2  10624  fzonn0p1p1  10642  swrdf  11442  pfxccatin12lem4  11513  resqrexlemover  11791  fisum0diag2  12232  dvdsnegb  12593  muldvds1  12601  muldvds2  12602  dvdscmul  12603  dvdsmulc  12604  dvds2add  12610  dvds2sub  12611  dvdstr  12613  addmodlteqALT  12644  divalgb  12710  ndvdsadd  12716  absmulgcd  12812  rpmulgcd  12821  cncongr2  12900  hashdvds  13021  pythagtriplem1  13066  mulgmodid  14015  nmzsubg  14064  assa2ass  15060  psrbagconf1o  15116  clwwlknccat  16786