Proof of Theorem 3elpr2eq
Step | Hyp | Ref
| Expression |
1 | | elpri 4588 |
. . 3
⊢ (𝑋 ∈ {𝐴, 𝐵} → (𝑋 = 𝐴 ∨ 𝑋 = 𝐵)) |
2 | | elpri 4588 |
. . 3
⊢ (𝑌 ∈ {𝐴, 𝐵} → (𝑌 = 𝐴 ∨ 𝑌 = 𝐵)) |
3 | | elpri 4588 |
. . 3
⊢ (𝑍 ∈ {𝐴, 𝐵} → (𝑍 = 𝐴 ∨ 𝑍 = 𝐵)) |
4 | | eqtr3 2765 |
. . . . . . . . . . 11
⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → 𝑍 = 𝑋) |
5 | | eqneqall 2955 |
. . . . . . . . . . 11
⊢ (𝑍 = 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)) |
6 | 4, 5 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)) |
7 | 6 | adantld 490 |
. . . . . . . . 9
⊢ ((𝑍 = 𝐴 ∧ 𝑋 = 𝐴) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)) |
8 | 7 | ex 412 |
. . . . . . . 8
⊢ (𝑍 = 𝐴 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))) |
9 | 8 | a1d 25 |
. . . . . . 7
⊢ (𝑍 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
10 | | eqtr3 2765 |
. . . . . . . . . . . . 13
⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → 𝑌 = 𝑋) |
11 | | eqneqall 2955 |
. . . . . . . . . . . . 13
⊢ (𝑌 = 𝑋 → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))) |
13 | 12 | impd 410 |
. . . . . . . . . . 11
⊢ ((𝑌 = 𝐴 ∧ 𝑋 = 𝐴) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)) |
14 | 13 | ex 412 |
. . . . . . . . . 10
⊢ (𝑌 = 𝐴 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))) |
15 | 14 | a1d 25 |
. . . . . . . . 9
⊢ (𝑌 = 𝐴 → (𝑍 = 𝐵 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
16 | | eqtr3 2765 |
. . . . . . . . . . 11
⊢ ((𝑌 = 𝐵 ∧ 𝑍 = 𝐵) → 𝑌 = 𝑍) |
17 | 16 | 2a1d 26 |
. . . . . . . . . 10
⊢ ((𝑌 = 𝐵 ∧ 𝑍 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))) |
18 | 17 | ex 412 |
. . . . . . . . 9
⊢ (𝑌 = 𝐵 → (𝑍 = 𝐵 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
19 | 15, 18 | jaoi 853 |
. . . . . . . 8
⊢ ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑍 = 𝐵 → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
20 | 19 | com12 32 |
. . . . . . 7
⊢ (𝑍 = 𝐵 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
21 | 9, 20 | jaoi 853 |
. . . . . 6
⊢ ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐴 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
22 | 21 | com13 88 |
. . . . 5
⊢ (𝑋 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
23 | | eqtr3 2765 |
. . . . . . . . . . 11
⊢ ((𝑌 = 𝐴 ∧ 𝑍 = 𝐴) → 𝑌 = 𝑍) |
24 | 23 | 2a1d 26 |
. . . . . . . . . 10
⊢ ((𝑌 = 𝐴 ∧ 𝑍 = 𝐴) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))) |
25 | 24 | ex 412 |
. . . . . . . . 9
⊢ (𝑌 = 𝐴 → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
26 | | eqtr3 2765 |
. . . . . . . . . . . . 13
⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → 𝑌 = 𝑋) |
27 | 26, 11 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → (𝑌 ≠ 𝑋 → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍))) |
28 | 27 | impd 410 |
. . . . . . . . . . 11
⊢ ((𝑌 = 𝐵 ∧ 𝑋 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)) |
29 | 28 | ex 412 |
. . . . . . . . . 10
⊢ (𝑌 = 𝐵 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))) |
30 | 29 | a1d 25 |
. . . . . . . . 9
⊢ (𝑌 = 𝐵 → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
31 | 25, 30 | jaoi 853 |
. . . . . . . 8
⊢ ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑍 = 𝐴 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
32 | 31 | com12 32 |
. . . . . . 7
⊢ (𝑍 = 𝐴 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
33 | | eqtr3 2765 |
. . . . . . . . . . 11
⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → 𝑍 = 𝑋) |
34 | 33, 5 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → (𝑍 ≠ 𝑋 → 𝑌 = 𝑍)) |
35 | 34 | adantld 490 |
. . . . . . . . 9
⊢ ((𝑍 = 𝐵 ∧ 𝑋 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)) |
36 | 35 | ex 412 |
. . . . . . . 8
⊢ (𝑍 = 𝐵 → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍))) |
37 | 36 | a1d 25 |
. . . . . . 7
⊢ (𝑍 = 𝐵 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
38 | 32, 37 | jaoi 853 |
. . . . . 6
⊢ ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → (𝑋 = 𝐵 → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
39 | 38 | com13 88 |
. . . . 5
⊢ (𝑋 = 𝐵 → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
40 | 22, 39 | jaoi 853 |
. . . 4
⊢ ((𝑋 = 𝐴 ∨ 𝑋 = 𝐵) → ((𝑌 = 𝐴 ∨ 𝑌 = 𝐵) → ((𝑍 = 𝐴 ∨ 𝑍 = 𝐵) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)))) |
41 | 40 | 3imp 1109 |
. . 3
⊢ (((𝑋 = 𝐴 ∨ 𝑋 = 𝐵) ∧ (𝑌 = 𝐴 ∨ 𝑌 = 𝐵) ∧ (𝑍 = 𝐴 ∨ 𝑍 = 𝐵)) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)) |
42 | 1, 2, 3, 41 | syl3an 1158 |
. 2
⊢ ((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) → ((𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋) → 𝑌 = 𝑍)) |
43 | 42 | imp 406 |
1
⊢ (((𝑋 ∈ {𝐴, 𝐵} ∧ 𝑌 ∈ {𝐴, 𝐵} ∧ 𝑍 ∈ {𝐴, 𝐵}) ∧ (𝑌 ≠ 𝑋 ∧ 𝑍 ≠ 𝑋)) → 𝑌 = 𝑍) |