Theorem syl8ib

Description: A syllogism rule of inference. The second premise is used to replace the consequent of the first premise. (Contributed by NM, 1-Aug-1994)

	Ref	Expression
Hypotheses	syl8ib.1	$$⊢\phi \to \left(\psi \to \left(\chi \to \theta \right)\right)$$
	syl8ib.2	$$⊢\theta \leftrightarrow \tau$$
Assertion	syl8ib	$$⊢\phi \to \left(\psi \to \left(\chi \to \tau \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		syl8ib.1	$$⊢\phi \to \left(\psi \to \left(\chi \to \theta \right)\right)$$
2		syl8ib.2	$$⊢\theta \leftrightarrow \tau$$
3	2	biimpi	$$⊢\theta \to \tau$$
4	1 3	syl8	$$⊢\phi \to \left(\psi \to \left(\chi \to \tau \right)\right)$$