Theorem syl3an 1320

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl2an3an  1339  funtpg  5432  ftpg  5899  eloprabga  6175  prfidisj  7234  djuenun  7568  addasspig  7697  mulasspig  7699  distrpig  7700  addcanpig  7701  mulcanpig  7702  ltapig  7705  distrnqg  7754  distrnq0  7826  cnegexlem2  8502  zletr  9696  zdivadd  9737  xaddass  10273  iooneg  10392  zltaddlt1le  10412  fzen  10449  fzaddel  10467  fzrev  10493  fzrevral2  10515  fzshftral  10517  fzosubel2  10615  fzonn0p1p1  10633  swrdf  11429  pfxccatin12lem4  11500  resqrexlemover  11778  fisum0diag2  12216  dvdsnegb  12577  muldvds1  12585  muldvds2  12586  dvdscmul  12587  dvdsmulc  12588  dvds2add  12594  dvds2sub  12595  dvdstr  12597  addmodlteqALT  12628  divalgb  12694  ndvdsadd  12700  absmulgcd  12796  rpmulgcd  12805  cncongr2  12884  hashdvds  13001  pythagtriplem1  13046  mulgmodid  13966  nmzsubg  14015  assa2ass  15011  psrbagconf1o  15066  clwwlknccat  16676