Theorem syl3an 1280

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

Syntax hints:   → wi 4   ∧ w3a 978

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 980

This theorem is referenced by:  syl2an3an  1298  funtpg  5268  ftpg  5701  eloprabga  5962  prfidisj  6926  djuenun  7211  addasspig  7329  mulasspig  7331  distrpig  7332  addcanpig  7333  mulcanpig  7334  ltapig  7337  distrnqg  7386  distrnq0  7458  cnegexlem2  8133  zletr  9302  zdivadd  9342  xaddass  9869  iooneg  9988  zltaddlt1le  10007  fzen  10043  fzaddel  10059  fzrev  10084  fzrevral2  10106  fzshftral  10108  fzosubel2  10195  fzonn0p1p1  10213  resqrexlemover  11019  fisum0diag2  11455  dvdsnegb  11815  muldvds1  11823  muldvds2  11824  dvdscmul  11825  dvdsmulc  11826  dvds2add  11832  dvds2sub  11833  dvdstr  11835  addmodlteqALT  11865  divalgb  11930  ndvdsadd  11936  absmulgcd  12018  rpmulgcd  12027  cncongr2  12104  hashdvds  12221  pythagtriplem1  12265  mulgmodid  13022  nmzsubg  13070