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  5381  ftpg  5838  eloprabga  6108  prfidisj  7119  djuenun  7427  addasspig  7550  mulasspig  7552  distrpig  7553  addcanpig  7554  mulcanpig  7555  ltapig  7558  distrnqg  7607  distrnq0  7679  cnegexlem2  8355  zletr  9529  zdivadd  9569  xaddass  10104  iooneg  10223  zltaddlt1le  10242  fzen  10278  fzaddel  10294  fzrev  10319  fzrevral2  10341  fzshftral  10343  fzosubel2  10441  fzonn0p1p1  10459  swrdf  11237  pfxccatin12lem4  11308  resqrexlemover  11572  fisum0diag2  12010  dvdsnegb  12371  muldvds1  12379  muldvds2  12380  dvdscmul  12381  dvdsmulc  12382  dvds2add  12388  dvds2sub  12389  dvdstr  12391  addmodlteqALT  12422  divalgb  12488  ndvdsadd  12494  absmulgcd  12590  rpmulgcd  12599  cncongr2  12678  hashdvds  12795  pythagtriplem1  12840  mulgmodid  13750  nmzsubg  13799  clwwlknccat  16277