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  5310  ftpg  5749  eloprabga  6013  prfidisj  6997  djuenun  7295  addasspig  7414  mulasspig  7416  distrpig  7417  addcanpig  7418  mulcanpig  7419  ltapig  7422  distrnqg  7471  distrnq0  7543  cnegexlem2  8219  zletr  9392  zdivadd  9432  xaddass  9961  iooneg  10080  zltaddlt1le  10099  fzen  10135  fzaddel  10151  fzrev  10176  fzrevral2  10198  fzshftral  10200  fzosubel2  10288  fzonn0p1p1  10306  resqrexlemover  11192  fisum0diag2  11629  dvdsnegb  11990  muldvds1  11998  muldvds2  11999  dvdscmul  12000  dvdsmulc  12001  dvds2add  12007  dvds2sub  12008  dvdstr  12010  addmodlteqALT  12041  divalgb  12107  ndvdsadd  12113  absmulgcd  12209  rpmulgcd  12218  cncongr2  12297  hashdvds  12414  pythagtriplem1  12459  mulgmodid  13367  nmzsubg  13416