Theorem impbid21d

Description: Deduce an equivalence from two implications. (Contributed by Wolf Lammen, 12-May-2013)

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

Proof

Step	Hyp	Ref	Expression
1		impbid21d.1	|- ( ps -> ( ch -> th ) )
2		impbid21d.2	|- ( ph -> ( th -> ch ) )
3		impbi	|- ( ( ch -> th ) -> ( ( th -> ch ) -> ( ch <-> th ) ) )
4	1 2 3	syl2imc	|- ( ph -> ( ps -> ( ch <-> th ) ) )