Theorem syl3an 1259

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

Syntax hints:   → wi 4   ∧ w3a 963

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

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

This theorem is referenced by:  syl2an3an  1277  funtpg  5182  ftpg  5612  eloprabga  5866  prfidisj  6823  djuenun  7085  addasspig  7162  mulasspig  7164  distrpig  7165  addcanpig  7166  mulcanpig  7167  ltapig  7170  distrnqg  7219  distrnq0  7291  cnegexlem2  7962  zletr  9127  zdivadd  9164  xaddass  9682  iooneg  9801  zltaddlt1le  9820  fzen  9854  fzaddel  9870  fzrev  9895  fzrevral2  9917  fzshftral  9919  fzosubel2  10003  fzonn0p1p1  10021  resqrexlemover  10814  fisum0diag2  11248  dvdsnegb  11546  muldvds1  11554  muldvds2  11555  dvdscmul  11556  dvdsmulc  11557  dvds2add  11563  dvds2sub  11564  dvdstr  11566  addmodlteqALT  11593  divalgb  11658  ndvdsadd  11664  absmulgcd  11741  rpmulgcd  11750  cncongr2  11821  hashdvds  11933