Theorem syl3an 1258

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

Syntax hints:   → wi 4   ∧ w3a 962

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

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  syl2an3an  1276  funtpg  5169  ftpg  5597  eloprabga  5851  prfidisj  6808  djuenun  7061  addasspig  7131  mulasspig  7133  distrpig  7134  addcanpig  7135  mulcanpig  7136  ltapig  7139  distrnqg  7188  distrnq0  7260  cnegexlem2  7931  zletr  9096  zdivadd  9133  xaddass  9645  iooneg  9764  zltaddlt1le  9782  fzen  9816  fzaddel  9832  fzrev  9857  fzrevral2  9879  fzshftral  9881  fzosubel2  9965  fzonn0p1p1  9983  resqrexlemover  10775  fisum0diag2  11209  dvdsnegb  11499  muldvds1  11507  muldvds2  11508  dvdscmul  11509  dvdsmulc  11510  dvds2add  11516  dvds2sub  11517  dvdstr  11519  addmodlteqALT  11546  divalgb  11611  ndvdsadd  11617  absmulgcd  11694  rpmulgcd  11703  cncongr2  11774  hashdvds  11886