Theorem elimhyp

Description: Eliminate a hypothesis containing class variable A when it is known for a specific class B . For more information, see comments in dedth . (Contributed by NM, 15-May-1999)

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

Proof

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