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  10475  fzosplitsnm1  10629  fzofzp1  10647  fzostep1  10658  bcm1k  11200  pfxccatpfx2  11511  climuni  12061  serf0  12120  fsumparts  12239  hashiun  12247  oddprm  13040  znzrh2  14983  znf1o  14988  znidom  14994  hmeores  15418  gausslemma2dlem0c  16182  gausslemma2dlem0e  16184  gausslemma2dlem1a  16189  eupthvdres  16728