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