Theorem syl3an 1313

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

Syntax hints:   → wi 4   ∧ w3a 1002

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 1004

This theorem is referenced by:  syl2an3an  1332  funtpg  5372  ftpg  5827  eloprabga  6097  prfidisj  7097  djuenun  7402  addasspig  7525  mulasspig  7527  distrpig  7528  addcanpig  7529  mulcanpig  7530  ltapig  7533  distrnqg  7582  distrnq0  7654  cnegexlem2  8330  zletr  9504  zdivadd  9544  xaddass  10073  iooneg  10192  zltaddlt1le  10211  fzen  10247  fzaddel  10263  fzrev  10288  fzrevral2  10310  fzshftral  10312  fzosubel2  10409  fzonn0p1p1  10427  swrdf  11195  pfxccatin12lem4  11266  resqrexlemover  11529  fisum0diag2  11966  dvdsnegb  12327  muldvds1  12335  muldvds2  12336  dvdscmul  12337  dvdsmulc  12338  dvds2add  12344  dvds2sub  12345  dvdstr  12347  addmodlteqALT  12378  divalgb  12444  ndvdsadd  12450  absmulgcd  12546  rpmulgcd  12555  cncongr2  12634  hashdvds  12751  pythagtriplem1  12796  mulgmodid  13706  nmzsubg  13755