Theorem 4syl 18

Description: Inference chaining three syllogisms. The use of this theorem is marked "discouraged" because it can cause the "minimize" command to have very long run times. However, feel free to use "minimize 4syl /override" if you wish. (Contributed by BJ, 14-Jul-2018.) (New usage is discouraged.)

Hypotheses

Ref	Expression
4syl.1	⊢ (𝜑 → 𝜓)
4syl.2	⊢ (𝜓 → 𝜒)
4syl.3	⊢ (𝜒 → 𝜃)
4syl.4	⊢ (𝜃 → 𝜏)

Assertion

Ref	Expression
4syl	⊢ (𝜑 → 𝜏)

Proof of Theorem 4syl

Step	Hyp	Ref	Expression
1		4syl.1	. . 3 ⊢ (𝜑 → 𝜓)
2		4syl.2	. . 3 ⊢ (𝜓 → 𝜒)
3		4syl.3	. . 3 ⊢ (𝜒 → 𝜃)
4	1, 2, 3	3syl 17	. 2 ⊢ (𝜑 → 𝜃)
5		4syl.4	. 2 ⊢ (𝜃 → 𝜏)
6	4, 5	syl 14	1 ⊢ (𝜑 → 𝜏)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  f1ocnvfvrneq  5988  fcof1o  5995  isoselem  6026  isose  6027  tposss  6517  smoiso  6573  fzssp1  10484  fzosplitsnm1  10638  fzofzp1  10656  fzostep1  10667  bcm1k  11213  pfxccatpfx2  11524  climuni  12077  serf0  12136  fsumparts  12255  hashiun  12263  oddprm  13060  znzrh2  15032  znf1o  15037  znidom  15043  hmeores  15468  ppinprm  16182  chtnprm  16184  gausslemma2dlem0c  16292  gausslemma2dlem0e  16294  gausslemma2dlem1a  16299  eupthvdres  16838