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  5991  fcof1o  5998  isoselem  6029  isose  6030  tposss  6521  smoiso  6577  fzssp1  10491  fzosplitsnm1  10645  fzofzp1  10663  fzostep1  10674  bcm1k  11221  pfxccatpfx2  11532  climuni  12085  serf0  12144  fsumparts  12263  hashiun  12271  oddprm  13068  znzrh2  15091  znf1o  15096  znidom  15102  hmeores  15553  ppinprm  16272  chtnprm  16274  gausslemma2dlem0c  16387  gausslemma2dlem0e  16389  gausslemma2dlem1a  16394  eupthvdres  16933