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  11724  fisum0diag2  12162  dvdsnegb  12523  muldvds1  12531  muldvds2  12532  dvdscmul  12533  dvdsmulc  12534  dvds2add  12540  dvds2sub  12541  dvdstr  12543  addmodlteqALT  12574  divalgb  12640  ndvdsadd  12646  absmulgcd  12742  rpmulgcd  12751  cncongr2  12830  hashdvds  12947  pythagtriplem1  12992  mulgmodid  13918  nmzsubg  13967  psrbagconf1o  14958  clwwlknccat  16548