Theorem bj-syl66ib

Description: A mixed syllogism inference derived from syl6ib . In addition to bj-dvelimdv1 , it can also shorten alexsubALTlem4 (4821>4812), supsrlem (2868>2863). (Contributed by BJ, 20-Oct-2021)

	Ref	Expression
Hypotheses	bj-syl66ib.1	⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) )
	bj-syl66ib.2	⊢ ( 𝜃 → 𝜏 )
	bj-syl66ib.3	⊢ ( 𝜏 ↔ 𝜒 )
Assertion	bj-syl66ib	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		bj-syl66ib.1	⊢ ( 𝜑 → ( 𝜓 → 𝜃 ) )
2		bj-syl66ib.2	⊢ ( 𝜃 → 𝜏 )
3		bj-syl66ib.3	⊢ ( 𝜏 ↔ 𝜒 )
4	1 2	syl6	⊢ ( 𝜑 → ( 𝜓 → 𝜏 ) )
5	4 3	syl6ib	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )