Theorem elimhyp2v

Description: Eliminate a hypothesis containing 2 class variables. (Contributed by NM, 14-Aug-1999)

	Ref	Expression
Hypotheses	elimhyp2v.1	|- ( A = if ( ph , A , C ) -> ( ph <-> ch ) )
	elimhyp2v.2	|- ( B = if ( ph , B , D ) -> ( ch <-> th ) )
	elimhyp2v.3	|- ( C = if ( ph , A , C ) -> ( ta <-> et ) )
	elimhyp2v.4	|- ( D = if ( ph , B , D ) -> ( et <-> th ) )
	elimhyp2v.5	|- ta
Assertion	elimhyp2v	|- th

Proof

Step	Hyp	Ref	Expression
1		elimhyp2v.1	|- ( A = if ( ph , A , C ) -> ( ph <-> ch ) )
2		elimhyp2v.2	|- ( B = if ( ph , B , D ) -> ( ch <-> th ) )
3		elimhyp2v.3	|- ( C = if ( ph , A , C ) -> ( ta <-> et ) )
4		elimhyp2v.4	|- ( D = if ( ph , B , D ) -> ( et <-> th ) )
5		elimhyp2v.5	|- ta
6		iftrue	|- ( ph -> if ( ph , A , C ) = A )
7	6	eqcomd	|- ( ph -> A = if ( ph , A , C ) )
8	7 1	syl	|- ( ph -> ( ph <-> ch ) )
9		iftrue	|- ( ph -> if ( ph , B , D ) = B )
10	9	eqcomd	|- ( ph -> B = if ( ph , B , D ) )
11	10 2	syl	|- ( ph -> ( ch <-> th ) )
12	8 11	bitrd	|- ( ph -> ( ph <-> th ) )
13	12	ibi	|- ( ph -> th )
14		iffalse	|- ( -. ph -> if ( ph , A , C ) = C )
15	14	eqcomd	|- ( -. ph -> C = if ( ph , A , C ) )
16	15 3	syl	|- ( -. ph -> ( ta <-> et ) )
17		iffalse	|- ( -. ph -> if ( ph , B , D ) = D )
18	17	eqcomd	|- ( -. ph -> D = if ( ph , B , D ) )
19	18 4	syl	|- ( -. ph -> ( et <-> th ) )
20	16 19	bitrd	|- ( -. ph -> ( ta <-> th ) )
21	5 20	mpbii	|- ( -. ph -> th )
22	13 21	pm2.61i	|- th