Theorem impbidd

Description: Deduce an equivalence from two implications. Double deduction associated with impbi and impbii . Deduction associated with impbid . (Contributed by Rodolfo Medina, 12-Oct-2010)

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

Proof

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