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 ⊢ ((𝜑 ∧ 𝜒 ∧ 𝜏) → 𝜁)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  syl2an3an  1339  funtpg  5435  ftpg  5902  eloprabga  6178  prfidisj  7239  djuenun  7575  addasspig  7704  mulasspig  7706  distrpig  7707  addcanpig  7708  mulcanpig  7709  ltapig  7712  distrnqg  7761  distrnq0  7833  cnegexlem2  8510  zletr  9706  zdivadd  9747  xaddass  10289  iooneg  10408  zltaddlt1le  10428  fzen  10465  fzaddel  10483  fzrev  10509  fzrevral2  10531  fzshftral  10533  fzosubel2  10631  fzonn0p1p1  10649  swrdf  11450  pfxccatin12lem4  11521  resqrexlemover  11799  fisum0diag2  12240  dvdsnegb  12601  muldvds1  12609  muldvds2  12610  dvdscmul  12611  dvdsmulc  12612  dvds2add  12618  dvds2sub  12619  dvdstr  12621  addmodlteqALT  12652  divalgb  12718  ndvdsadd  12724  absmulgcd  12820  rpmulgcd  12829  cncongr2  12908  hashdvds  13029  pythagtriplem1  13074  mulgmodid  14024  nmzsubg  14073  assa2ass  15119  psrbagconf1o  15179  gsumbagdiaglem  15180  psrass1filem  15182  psrass1fi  15206  clwwlknccat  16881