Theorem syl3an 1291

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

Syntax hints:   → wi 4   ∧ w3a 980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  syl2an3an  1309  funtpg  5309  ftpg  5746  eloprabga  6009  prfidisj  6988  djuenun  7279  addasspig  7397  mulasspig  7399  distrpig  7400  addcanpig  7401  mulcanpig  7402  ltapig  7405  distrnqg  7454  distrnq0  7526  cnegexlem2  8202  zletr  9375  zdivadd  9415  xaddass  9944  iooneg  10063  zltaddlt1le  10082  fzen  10118  fzaddel  10134  fzrev  10159  fzrevral2  10181  fzshftral  10183  fzosubel2  10271  fzonn0p1p1  10289  resqrexlemover  11175  fisum0diag2  11612  dvdsnegb  11973  muldvds1  11981  muldvds2  11982  dvdscmul  11983  dvdsmulc  11984  dvds2add  11990  dvds2sub  11991  dvdstr  11993  addmodlteqALT  12024  divalgb  12090  ndvdsadd  12096  absmulgcd  12184  rpmulgcd  12193  cncongr2  12272  hashdvds  12389  pythagtriplem1  12434  mulgmodid  13291  nmzsubg  13340