Theorem syl3an 1291

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

Syntax hints:   → wi 4   ∧ w3a 980

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 982

This theorem is referenced by:  syl2an3an  1309  funtpg  5310  ftpg  5749  eloprabga  6013  prfidisj  6997  djuenun  7297  addasspig  7416  mulasspig  7418  distrpig  7419  addcanpig  7420  mulcanpig  7421  ltapig  7424  distrnqg  7473  distrnq0  7545  cnegexlem2  8221  zletr  9394  zdivadd  9434  xaddass  9963  iooneg  10082  zltaddlt1le  10101  fzen  10137  fzaddel  10153  fzrev  10178  fzrevral2  10200  fzshftral  10202  fzosubel2  10290  fzonn0p1p1  10308  resqrexlemover  11194  fisum0diag2  11631  dvdsnegb  11992  muldvds1  12000  muldvds2  12001  dvdscmul  12002  dvdsmulc  12003  dvds2add  12009  dvds2sub  12010  dvdstr  12012  addmodlteqALT  12043  divalgb  12109  ndvdsadd  12115  absmulgcd  12211  rpmulgcd  12220  cncongr2  12299  hashdvds  12416  pythagtriplem1  12461  mulgmodid  13369  nmzsubg  13418