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  5406  ftpg  5867  eloprabga  6139  prfidisj  7186  djuenun  7518  addasspig  7644  mulasspig  7646  distrpig  7647  addcanpig  7648  mulcanpig  7649  ltapig  7652  distrnqg  7701  distrnq0  7773  cnegexlem2  8448  zletr  9626  zdivadd  9666  xaddass  10201  iooneg  10320  zltaddlt1le  10340  fzen  10376  fzaddel  10392  fzrev  10417  fzrevral2  10439  fzshftral  10441  fzosubel2  10539  fzonn0p1p1  10557  swrdf  11343  pfxccatin12lem4  11414  resqrexlemover  11691  fisum0diag2  12129  dvdsnegb  12490  muldvds1  12498  muldvds2  12499  dvdscmul  12500  dvdsmulc  12501  dvds2add  12507  dvds2sub  12508  dvdstr  12510  addmodlteqALT  12541  divalgb  12607  ndvdsadd  12613  absmulgcd  12709  rpmulgcd  12718  cncongr2  12797  hashdvds  12914  pythagtriplem1  12959  mulgmodid  13870  nmzsubg  13919  psrbagconf1o  14820  clwwlknccat  16410