Theorem bitri

Description: An inference from transitive law for logical equivalence. (Contributed by NM, 3-Jan-1993) (Proof shortened by Wolf Lammen, 13-Oct-2012)

	Ref	Expression
Hypotheses	bitri.1	$$⊢\phi \leftrightarrow \psi$$
	bitri.2	$$⊢\psi \leftrightarrow \chi$$
Assertion	bitri	$$⊢\phi \leftrightarrow \chi$$

Proof

Step	Hyp	Ref	Expression
1		bitri.1	$$⊢\phi \leftrightarrow \psi$$
2		bitri.2	$$⊢\psi \leftrightarrow \chi$$
3	1 2	sylbb	$$⊢\phi \to \chi$$
4	1 2	sylbbr	$$⊢\chi \to \phi$$
5	3 4	impbii	$$⊢\phi \leftrightarrow \chi$$