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  8465  zletr  9644  zdivadd  9685  xaddass  10221  iooneg  10340  zltaddlt1le  10360  fzen  10397  fzaddel  10414  fzrev  10440  fzrevral2  10462  fzshftral  10464  fzosubel2  10562  fzonn0p1p1  10580  swrdf  11372  pfxccatin12lem4  11443  resqrexlemover  11720  fisum0diag2  12158  dvdsnegb  12519  muldvds1  12527  muldvds2  12528  dvdscmul  12529  dvdsmulc  12530  dvds2add  12536  dvds2sub  12537  dvdstr  12539  addmodlteqALT  12570  divalgb  12636  ndvdsadd  12642  absmulgcd  12738  rpmulgcd  12747  cncongr2  12826  hashdvds  12943  pythagtriplem1  12988  mulgmodid  13962  nmzsubg  14011  psrbagconf1o  14940  clwwlknccat  16530