Theorem syl3an 1292

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

Syntax hints:   → wi 4   ∧ w3a 981

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 983

This theorem is referenced by:  syl2an3an  1311  funtpg  5330  ftpg  5775  eloprabga  6039  prfidisj  7031  djuenun  7331  addasspig  7450  mulasspig  7452  distrpig  7453  addcanpig  7454  mulcanpig  7455  ltapig  7458  distrnqg  7507  distrnq0  7579  cnegexlem2  8255  zletr  9429  zdivadd  9469  xaddass  9998  iooneg  10117  zltaddlt1le  10136  fzen  10172  fzaddel  10188  fzrev  10213  fzrevral2  10235  fzshftral  10237  fzosubel2  10331  fzonn0p1p1  10349  swrdf  11116  resqrexlemover  11365  fisum0diag2  11802  dvdsnegb  12163  muldvds1  12171  muldvds2  12172  dvdscmul  12173  dvdsmulc  12174  dvds2add  12180  dvds2sub  12181  dvdstr  12183  addmodlteqALT  12214  divalgb  12280  ndvdsadd  12286  absmulgcd  12382  rpmulgcd  12391  cncongr2  12470  hashdvds  12587  pythagtriplem1  12632  mulgmodid  13541  nmzsubg  13590