This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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