Theorem elimhyp3v

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

	Ref	Expression
Hypotheses	elimhyp3v.1	|- ( A = if ( ph , A , D ) -> ( ph <-> ch ) )
	elimhyp3v.2	|- ( B = if ( ph , B , R ) -> ( ch <-> th ) )
	elimhyp3v.3	|- ( C = if ( ph , C , S ) -> ( th <-> ta ) )
	elimhyp3v.4	|- ( D = if ( ph , A , D ) -> ( et <-> ze ) )
	elimhyp3v.5	|- ( R = if ( ph , B , R ) -> ( ze <-> si ) )
	elimhyp3v.6	|- ( S = if ( ph , C , S ) -> ( si <-> ta ) )
	elimhyp3v.7	|- et
Assertion	elimhyp3v	|- ta

Proof

Step	Hyp	Ref	Expression
1		elimhyp3v.1	|- ( A = if ( ph , A , D ) -> ( ph <-> ch ) )
2		elimhyp3v.2	|- ( B = if ( ph , B , R ) -> ( ch <-> th ) )
3		elimhyp3v.3	|- ( C = if ( ph , C , S ) -> ( th <-> ta ) )
4		elimhyp3v.4	|- ( D = if ( ph , A , D ) -> ( et <-> ze ) )
5		elimhyp3v.5	|- ( R = if ( ph , B , R ) -> ( ze <-> si ) )
6		elimhyp3v.6	|- ( S = if ( ph , C , S ) -> ( si <-> ta ) )
7		elimhyp3v.7	|- et
8		iftrue	|- ( ph -> if ( ph , A , D ) = A )
9	8	eqcomd	|- ( ph -> A = if ( ph , A , D ) )
10	9 1	syl	|- ( ph -> ( ph <-> ch ) )
11		iftrue	|- ( ph -> if ( ph , B , R ) = B )
12	11	eqcomd	|- ( ph -> B = if ( ph , B , R ) )
13	12 2	syl	|- ( ph -> ( ch <-> th ) )
14		iftrue	|- ( ph -> if ( ph , C , S ) = C )
15	14	eqcomd	|- ( ph -> C = if ( ph , C , S ) )
16	15 3	syl	|- ( ph -> ( th <-> ta ) )
17	10 13 16	3bitrd	|- ( ph -> ( ph <-> ta ) )
18	17	ibi	|- ( ph -> ta )
19		iffalse	|- ( -. ph -> if ( ph , A , D ) = D )
20	19	eqcomd	|- ( -. ph -> D = if ( ph , A , D ) )
21	20 4	syl	|- ( -. ph -> ( et <-> ze ) )
22		iffalse	|- ( -. ph -> if ( ph , B , R ) = R )
23	22	eqcomd	|- ( -. ph -> R = if ( ph , B , R ) )
24	23 5	syl	|- ( -. ph -> ( ze <-> si ) )
25		iffalse	|- ( -. ph -> if ( ph , C , S ) = S )
26	25	eqcomd	|- ( -. ph -> S = if ( ph , C , S ) )
27	26 6	syl	|- ( -. ph -> ( si <-> ta ) )
28	21 24 27	3bitrd	|- ( -. ph -> ( et <-> ta ) )
29	7 28	mpbii	|- ( -. ph -> ta )
30	18 29	pm2.61i	|- ta