Theorem elimdhyp

Description: Version of elimhyp where the hypothesis is deduced from the final antecedent. See divalg for an example of its use. (Contributed by Paul Chapman, 25-Mar-2008)

	Ref	Expression
Hypotheses	elimdhyp.1	|- ( ph -> ps )
	elimdhyp.2	|- ( A = if ( ph , A , B ) -> ( ps <-> ch ) )
	elimdhyp.3	|- ( B = if ( ph , A , B ) -> ( th <-> ch ) )
	elimdhyp.4	|- th
Assertion	elimdhyp	|- ch

Proof

Step	Hyp	Ref	Expression
1		elimdhyp.1	|- ( ph -> ps )
2		elimdhyp.2	|- ( A = if ( ph , A , B ) -> ( ps <-> ch ) )
3		elimdhyp.3	|- ( B = if ( ph , A , B ) -> ( th <-> ch ) )
4		elimdhyp.4	|- th
5		iftrue	|- ( ph -> if ( ph , A , B ) = A )
6	5	eqcomd	|- ( ph -> A = if ( ph , A , B ) )
7	6 2	syl	|- ( ph -> ( ps <-> ch ) )
8	1 7	mpbid	|- ( ph -> ch )
9		iffalse	|- ( -. ph -> if ( ph , A , B ) = B )
10	9	eqcomd	|- ( -. ph -> B = if ( ph , A , B ) )
11	10 3	syl	|- ( -. ph -> ( th <-> ch ) )
12	4 11	mpbii	|- ( -. ph -> ch )
13	8 12	pm2.61i	|- ch