Theorem keephyp2v

Description: Keep a hypothesis containing 2 class variables (for use with the weak deduction theorem dedth ). (Contributed by NM, 16-Apr-2005)

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

Proof

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