Theorem 2thd

Description: Two truths are equivalent. Deduction form. (Contributed by NM, 3-Jun-2012)

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

Proof

Step	Hyp	Ref	Expression
1		2thd.1	|- ( ph -> ps )
2		2thd.2	|- ( ph -> ch )
3		pm5.1im	|- ( ps -> ( ch -> ( ps <-> ch ) ) )
4	1 2 3	sylc	|- ( ph -> ( ps <-> ch ) )