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	$$⊢\phi \to \left(\psi \to \theta \right)$$
	bj-syl66ib.2	$$⊢\theta \to \tau$$
	bj-syl66ib.3	$$⊢\tau \leftrightarrow \chi$$
Assertion	bj-syl66ib	$$⊢\phi \to \left(\psi \to \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		bj-syl66ib.1	$$⊢\phi \to \left(\psi \to \theta \right)$$
2		bj-syl66ib.2	$$⊢\theta \to \tau$$
3		bj-syl66ib.3	$$⊢\tau \leftrightarrow \chi$$
4	1 2	syl6	$$⊢\phi \to \left(\psi \to \tau \right)$$
5	4 3	syl6ib	$$⊢\phi \to \left(\psi \to \chi \right)$$