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  5378  ftpg  5833  eloprabga  6103  prfidisj  7114  djuenun  7420  addasspig  7543  mulasspig  7545  distrpig  7546  addcanpig  7547  mulcanpig  7548  ltapig  7551  distrnqg  7600  distrnq0  7672  cnegexlem2  8348  zletr  9522  zdivadd  9562  xaddass  10097  iooneg  10216  zltaddlt1le  10235  fzen  10271  fzaddel  10287  fzrev  10312  fzrevral2  10334  fzshftral  10336  fzosubel2  10433  fzonn0p1p1  10451  swrdf  11229  pfxccatin12lem4  11300  resqrexlemover  11564  fisum0diag2  12001  dvdsnegb  12362  muldvds1  12370  muldvds2  12371  dvdscmul  12372  dvdsmulc  12373  dvds2add  12379  dvds2sub  12380  dvdstr  12382  addmodlteqALT  12413  divalgb  12479  ndvdsadd  12485  absmulgcd  12581  rpmulgcd  12590  cncongr2  12669  hashdvds  12786  pythagtriplem1  12831  mulgmodid  13741  nmzsubg  13790  clwwlknccat  16232