Theorem 3bitr2i

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

	Ref	Expression
Hypotheses	3bitr2i.1	|- ( ph <-> ps )
	3bitr2i.2	|- ( ch <-> ps )
	3bitr2i.3	|- ( ch <-> th )
Assertion	3bitr2i	|- ( ph <-> th )

Proof

Step	Hyp	Ref	Expression
1		3bitr2i.1	|- ( ph <-> ps )
2		3bitr2i.2	|- ( ch <-> ps )
3		3bitr2i.3	|- ( ch <-> th )
4	1 2	bitr4i	|- ( ph <-> ch )
5	4 3	bitri	|- ( ph <-> th )