Theorem syl3an 1258

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

Syntax hints:   → wi 4   ∧ w3a 962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 964

This theorem is referenced by:  syl2an3an  1276  funtpg  5174  ftpg  5604  eloprabga  5858  prfidisj  6815  djuenun  7068  addasspig  7143  mulasspig  7145  distrpig  7146  addcanpig  7147  mulcanpig  7148  ltapig  7151  distrnqg  7200  distrnq0  7272  cnegexlem2  7943  zletr  9108  zdivadd  9145  xaddass  9657  iooneg  9776  zltaddlt1le  9794  fzen  9828  fzaddel  9844  fzrev  9869  fzrevral2  9891  fzshftral  9893  fzosubel2  9977  fzonn0p1p1  9995  resqrexlemover  10787  fisum0diag2  11221  dvdsnegb  11515  muldvds1  11523  muldvds2  11524  dvdscmul  11525  dvdsmulc  11526  dvds2add  11532  dvds2sub  11533  dvdstr  11535  addmodlteqALT  11562  divalgb  11627  ndvdsadd  11633  absmulgcd  11710  rpmulgcd  11719  cncongr2  11790  hashdvds  11902