This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elimhyp3v

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

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

Proof

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