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  5375  ftpg  5830  eloprabga  6100  prfidisj  7105  djuenun  7410  addasspig  7533  mulasspig  7535  distrpig  7536  addcanpig  7537  mulcanpig  7538  ltapig  7541  distrnqg  7590  distrnq0  7662  cnegexlem2  8338  zletr  9512  zdivadd  9552  xaddass  10082  iooneg  10201  zltaddlt1le  10220  fzen  10256  fzaddel  10272  fzrev  10297  fzrevral2  10319  fzshftral  10321  fzosubel2  10418  fzonn0p1p1  10436  swrdf  11208  pfxccatin12lem4  11279  resqrexlemover  11542  fisum0diag2  11979  dvdsnegb  12340  muldvds1  12348  muldvds2  12349  dvdscmul  12350  dvdsmulc  12351  dvds2add  12357  dvds2sub  12358  dvdstr  12360  addmodlteqALT  12391  divalgb  12457  ndvdsadd  12463  absmulgcd  12559  rpmulgcd  12568  cncongr2  12647  hashdvds  12764  pythagtriplem1  12809  mulgmodid  13719  nmzsubg  13768  clwwlknccat  16191