Theorem 3bitr3g

Description: More general version of 3bitr3i . Useful for converting definitions in a formula. (Contributed by NM, 4-Jun-1995)

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

Proof

Step	Hyp	Ref	Expression
1		3bitr3g.1	|- ( ph -> ( ps <-> ch ) )
2		3bitr3g.2	|- ( ps <-> th )
3		3bitr3g.3	|- ( ch <-> ta )
4	2 1	bitr3id	|- ( ph -> ( th <-> ch ) )
5	4 3	bitrdi	|- ( ph -> ( th <-> ta ) )