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

Metamath Proof Explorer

Theorem elimhyp4v

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

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

Proof

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