Theorem syl3an 1320

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

Syntax hints:   → wi 4   ∧ w3a 1009

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 1011

This theorem is referenced by:  syl2an3an  1339  funtpg  5430  ftpg  5893  eloprabga  6169  prfidisj  7228  djuenun  7562  addasspig  7691  mulasspig  7693  distrpig  7694  addcanpig  7695  mulcanpig  7696  ltapig  7699  distrnqg  7748  distrnq0  7820  cnegexlem2  8496  zletr  9677  zdivadd  9718  xaddass  10254  iooneg  10373  zltaddlt1le  10393  fzen  10430  fzaddel  10448  fzrev  10474  fzrevral2  10496  fzshftral  10498  fzosubel2  10596  fzonn0p1p1  10614  swrdf  11410  pfxccatin12lem4  11481  resqrexlemover  11759  fisum0diag2  12197  dvdsnegb  12558  muldvds1  12566  muldvds2  12567  dvdscmul  12568  dvdsmulc  12569  dvds2add  12575  dvds2sub  12576  dvdstr  12578  addmodlteqALT  12609  divalgb  12675  ndvdsadd  12681  absmulgcd  12777  rpmulgcd  12786  cncongr2  12865  hashdvds  12982  pythagtriplem1  13027  mulgmodid  13947  nmzsubg  13996  assa2ass  14992  psrbagconf1o  15047  clwwlknccat  16647