Theorem syl3an 1316

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

Syntax hints:   → wi 4   ∧ w3a 1005

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 1007

This theorem is referenced by:  syl2an3an  1335  funtpg  5412  ftpg  5873  eloprabga  6148  prfidisj  7200  djuenun  7532  addasspig  7661  mulasspig  7663  distrpig  7664  addcanpig  7665  mulcanpig  7666  ltapig  7669  distrnqg  7718  distrnq0  7790  cnegexlem2  8466  zletr  9647  zdivadd  9688  xaddass  10224  iooneg  10343  zltaddlt1le  10363  fzen  10400  fzaddel  10417  fzrev  10443  fzrevral2  10465  fzshftral  10467  fzosubel2  10565  fzonn0p1p1  10583  swrdf  11375  pfxccatin12lem4  11446  resqrexlemover  11723  fisum0diag2  12161  dvdsnegb  12522  muldvds1  12530  muldvds2  12531  dvdscmul  12532  dvdsmulc  12533  dvds2add  12539  dvds2sub  12540  dvdstr  12542  addmodlteqALT  12573  divalgb  12639  ndvdsadd  12645  absmulgcd  12741  rpmulgcd  12750  cncongr2  12829  hashdvds  12946  pythagtriplem1  12991  mulgmodid  13917  nmzsubg  13966  psrbagconf1o  14957  clwwlknccat  16547