Theorem 3bitr2i

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006)

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

Proof

Step	Hyp	Ref	Expression
1		3bitr2i.1	$$⊢\phi \leftrightarrow \psi$$
2		3bitr2i.2	$$⊢\chi \leftrightarrow \psi$$
3		3bitr2i.3	$$⊢\chi \leftrightarrow \theta$$
4	1 2	bitr4i	$$⊢\phi \leftrightarrow \chi$$
5	4 3	bitri	$$⊢\phi \leftrightarrow \theta$$