Theorem keephyp3v

Description: Keep a hypothesis containing 3 class variables. (Contributed by NM, 27-Sep-1999)

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

Proof

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