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  5435  ftpg  5902  eloprabga  6178  prfidisj  7240  djuenun  7575  addasspig  7704  mulasspig  7706  distrpig  7707  addcanpig  7708  mulcanpig  7709  ltapig  7712  distrnqg  7761  distrnq0  7833  cnegexlem2  8510  zletr  9704  zdivadd  9746  xaddass  10288  iooneg  10407  zltaddlt1le  10427  fzen  10464  fzaddel  10482  fzrev  10508  fzrevral2  10530  fzshftral  10532  fzosubel2  10630  fzonn0p1p1  10648  swrdf  11449  pfxccatin12lem4  11520  resqrexlemover  11798  fisum0diag2  12239  dvdsnegb  12600  muldvds1  12608  muldvds2  12609  dvdscmul  12610  dvdsmulc  12611  dvds2add  12617  dvds2sub  12618  dvdstr  12620  addmodlteqALT  12651  divalgb  12717  ndvdsadd  12723  absmulgcd  12819  rpmulgcd  12828  cncongr2  12907  hashdvds  13028  pythagtriplem1  13073  mulgmodid  14023  nmzsubg  14072  assa2ass  15118  psrbagconf1o  15177  gsumbagdiaglem  15194  psrass1filem  15196  psrass1fi  15221  clwwlknccat  16902