Theorem syl3an 1315

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

Syntax hints:   → wi 4   ∧ w3a 1004

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 1006

This theorem is referenced by:  syl2an3an  1334  funtpg  5383  ftpg  5841  eloprabga  6113  prfidisj  7124  djuenun  7432  addasspig  7555  mulasspig  7557  distrpig  7558  addcanpig  7559  mulcanpig  7560  ltapig  7563  distrnqg  7612  distrnq0  7684  cnegexlem2  8360  zletr  9534  zdivadd  9574  xaddass  10109  iooneg  10228  zltaddlt1le  10247  fzen  10283  fzaddel  10299  fzrev  10324  fzrevral2  10346  fzshftral  10348  fzosubel2  10446  fzonn0p1p1  10464  swrdf  11245  pfxccatin12lem4  11316  resqrexlemover  11593  fisum0diag2  12031  dvdsnegb  12392  muldvds1  12400  muldvds2  12401  dvdscmul  12402  dvdsmulc  12403  dvds2add  12409  dvds2sub  12410  dvdstr  12412  addmodlteqALT  12443  divalgb  12509  ndvdsadd  12515  absmulgcd  12611  rpmulgcd  12620  cncongr2  12699  hashdvds  12816  pythagtriplem1  12861  mulgmodid  13771  nmzsubg  13820  psrbagconf1o  14716  clwwlknccat  16303