Theorem syl3an 1217

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

Syntax hints:   → wi 4   ∧ w3a 925

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 927

This theorem is referenced by:  syl2an3an  1235  funtpg  5080  ftpg  5497  eloprabga  5751  prfidisj  6693  addasspig  6952  mulasspig  6954  distrpig  6955  addcanpig  6956  mulcanpig  6957  ltapig  6960  distrnqg  7009  distrnq0  7081  cnegexlem2  7721  zletr  8862  zdivadd  8898  iooneg  9468  zltaddlt1le  9486  fzen  9520  fzaddel  9536  fzrev  9561  fzrevral2  9583  fzshftral  9585  fzosubel2  9669  fzonn0p1p1  9687  resqrexlemover  10506  fisum0diag2  10904  dvdsnegb  11154  muldvds1  11162  muldvds2  11163  dvdscmul  11164  dvdsmulc  11165  dvds2add  11171  dvds2sub  11172  dvdstr  11174  addmodlteqALT  11201  divalgb  11266  ndvdsadd  11272  absmulgcd  11347  rpmulgcd  11356  cncongr2  11427  hashdvds  11538