Theorem 4syl

Description: Inference chaining three syllogisms syl . (Contributed by BJ, 14-Jul-2018) The use of this theorem is marked "discouraged" because it can cause the Metamath program "MM-PA> MINIMIZE__WITH *" command to have very long run times. However, feel free to use "MM-PA> MINIMIZE__WITH 4syl / OVERRIDE" if you wish. Remember to update the "discouraged" file if it gets used. (New usage is discouraged.)

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

Proof

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