Theorem 3imtr4i

Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication. (Contributed by NM, 3-Jan-1993)

	Ref	Expression
Hypotheses	3imtr4.1	$$⊢\phi \to \psi$$
	3imtr4.2	$$⊢\chi \leftrightarrow \phi$$
	3imtr4.3	$$⊢\theta \leftrightarrow \psi$$
Assertion	3imtr4i	$$⊢\chi \to \theta$$

Proof

Step	Hyp	Ref	Expression
1		3imtr4.1	$$⊢\phi \to \psi$$
2		3imtr4.2	$$⊢\chi \leftrightarrow \phi$$
3		3imtr4.3	$$⊢\theta \leftrightarrow \psi$$
4	2 1	sylbi	$$⊢\chi \to \psi$$
5	4 3	sylibr	$$⊢\chi \to \theta$$