Theorem syl3an 1294

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

Syntax hints:   → wi 4   ∧ w3a 983

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 985

This theorem is referenced by:  syl2an3an  1313  funtpg  5348  ftpg  5796  eloprabga  6062  prfidisj  7057  djuenun  7362  addasspig  7485  mulasspig  7487  distrpig  7488  addcanpig  7489  mulcanpig  7490  ltapig  7493  distrnqg  7542  distrnq0  7614  cnegexlem2  8290  zletr  9464  zdivadd  9504  xaddass  10033  iooneg  10152  zltaddlt1le  10171  fzen  10207  fzaddel  10223  fzrev  10248  fzrevral2  10270  fzshftral  10272  fzosubel2  10368  fzonn0p1p1  10386  swrdf  11153  pfxccatin12lem4  11224  resqrexlemover  11487  fisum0diag2  11924  dvdsnegb  12285  muldvds1  12293  muldvds2  12294  dvdscmul  12295  dvdsmulc  12296  dvds2add  12302  dvds2sub  12303  dvdstr  12305  addmodlteqALT  12336  divalgb  12402  ndvdsadd  12408  absmulgcd  12504  rpmulgcd  12513  cncongr2  12592  hashdvds  12709  pythagtriplem1  12754  mulgmodid  13664  nmzsubg  13713