Theorem bibi12i

Description: The equivalence of two equivalences. (Contributed by NM, 26-May-1993)

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

Proof

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