Theorem bibi1d

Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-1993)

	Ref	Expression
Hypothesis	imbid.1	|- ( ph -> ( ps <-> ch ) )
Assertion	bibi1d	|- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )

Proof

Step	Hyp	Ref	Expression
1		imbid.1	|- ( ph -> ( ps <-> ch ) )
2	1	bibi2d	|- ( ph -> ( ( th <-> ps ) <-> ( th <-> ch ) ) )
3		bicom	|- ( ( ps <-> th ) <-> ( th <-> ps ) )
4		bicom	|- ( ( ch <-> th ) <-> ( th <-> ch ) )
5	2 3 4	3bitr4g	|- ( ph -> ( ( ps <-> th ) <-> ( ch <-> th ) ) )