Theorem keephyp3v

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

	Ref	Expression
Hypotheses	keephyp3v.1	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜌 ↔ 𝜒 ) )
	keephyp3v.2	⊢ ( 𝐵 = if ( 𝜑 , 𝐵 , 𝑅 ) → ( 𝜒 ↔ 𝜃 ) )
	keephyp3v.3	⊢ ( 𝐶 = if ( 𝜑 , 𝐶 , 𝑆 ) → ( 𝜃 ↔ 𝜏 ) )
	keephyp3v.4	⊢ ( 𝐷 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜂 ↔ 𝜁 ) )
	keephyp3v.5	⊢ ( 𝑅 = if ( 𝜑 , 𝐵 , 𝑅 ) → ( 𝜁 ↔ 𝜎 ) )
	keephyp3v.6	⊢ ( 𝑆 = if ( 𝜑 , 𝐶 , 𝑆 ) → ( 𝜎 ↔ 𝜏 ) )
	keephyp3v.7	⊢ 𝜌
	keephyp3v.8	⊢ 𝜂
Assertion	keephyp3v	⊢ 𝜏

Proof

Step	Hyp	Ref	Expression
1		keephyp3v.1	⊢ ( 𝐴 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜌 ↔ 𝜒 ) )
2		keephyp3v.2	⊢ ( 𝐵 = if ( 𝜑 , 𝐵 , 𝑅 ) → ( 𝜒 ↔ 𝜃 ) )
3		keephyp3v.3	⊢ ( 𝐶 = if ( 𝜑 , 𝐶 , 𝑆 ) → ( 𝜃 ↔ 𝜏 ) )
4		keephyp3v.4	⊢ ( 𝐷 = if ( 𝜑 , 𝐴 , 𝐷 ) → ( 𝜂 ↔ 𝜁 ) )
5		keephyp3v.5	⊢ ( 𝑅 = if ( 𝜑 , 𝐵 , 𝑅 ) → ( 𝜁 ↔ 𝜎 ) )
6		keephyp3v.6	⊢ ( 𝑆 = if ( 𝜑 , 𝐶 , 𝑆 ) → ( 𝜎 ↔ 𝜏 ) )
7		keephyp3v.7	⊢ 𝜌
8		keephyp3v.8	⊢ 𝜂
9		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐴 , 𝐷 ) = 𝐴 )
10	9	eqcomd	⊢ ( 𝜑 → 𝐴 = if ( 𝜑 , 𝐴 , 𝐷 ) )
11	10 1	syl	⊢ ( 𝜑 → ( 𝜌 ↔ 𝜒 ) )
12		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐵 , 𝑅 ) = 𝐵 )
13	12	eqcomd	⊢ ( 𝜑 → 𝐵 = if ( 𝜑 , 𝐵 , 𝑅 ) )
14	13 2	syl	⊢ ( 𝜑 → ( 𝜒 ↔ 𝜃 ) )
15		iftrue	⊢ ( 𝜑 → if ( 𝜑 , 𝐶 , 𝑆 ) = 𝐶 )
16	15	eqcomd	⊢ ( 𝜑 → 𝐶 = if ( 𝜑 , 𝐶 , 𝑆 ) )
17	16 3	syl	⊢ ( 𝜑 → ( 𝜃 ↔ 𝜏 ) )
18	11 14 17	3bitrd	⊢ ( 𝜑 → ( 𝜌 ↔ 𝜏 ) )
19	7 18	mpbii	⊢ ( 𝜑 → 𝜏 )
20		iffalse	⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐴 , 𝐷 ) = 𝐷 )
21	20	eqcomd	⊢ ( ¬ 𝜑 → 𝐷 = if ( 𝜑 , 𝐴 , 𝐷 ) )
22	21 4	syl	⊢ ( ¬ 𝜑 → ( 𝜂 ↔ 𝜁 ) )
23		iffalse	⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐵 , 𝑅 ) = 𝑅 )
24	23	eqcomd	⊢ ( ¬ 𝜑 → 𝑅 = if ( 𝜑 , 𝐵 , 𝑅 ) )
25	24 5	syl	⊢ ( ¬ 𝜑 → ( 𝜁 ↔ 𝜎 ) )
26		iffalse	⊢ ( ¬ 𝜑 → if ( 𝜑 , 𝐶 , 𝑆 ) = 𝑆 )
27	26	eqcomd	⊢ ( ¬ 𝜑 → 𝑆 = if ( 𝜑 , 𝐶 , 𝑆 ) )
28	27 6	syl	⊢ ( ¬ 𝜑 → ( 𝜎 ↔ 𝜏 ) )
29	22 25 28	3bitrd	⊢ ( ¬ 𝜑 → ( 𝜂 ↔ 𝜏 ) )
30	8 29	mpbii	⊢ ( ¬ 𝜑 → 𝜏 )
31	19 30	pm2.61i	⊢ 𝜏