Proof of Theorem 2pm13.193
Step | Hyp | Ref
| Expression |
1 | | simpll 767 |
. . 3
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → 𝑥 = 𝑢) |
2 | | simplr 769 |
. . 3
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → 𝑦 = 𝑣) |
3 | | simpr 488 |
. . . . 5
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) |
4 | | sbequ2 2250 |
. . . . 5
⊢ (𝑥 = 𝑢 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑣 / 𝑦]𝜑)) |
5 | 1, 3, 4 | sylc 65 |
. . . 4
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → [𝑣 / 𝑦]𝜑) |
6 | | sbequ2 2250 |
. . . 4
⊢ (𝑦 = 𝑣 → ([𝑣 / 𝑦]𝜑 → 𝜑)) |
7 | 2, 5, 6 | sylc 65 |
. . 3
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → 𝜑) |
8 | 1, 2, 7 | jca31 518 |
. 2
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) |
9 | | simpll 767 |
. . 3
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → 𝑥 = 𝑢) |
10 | | simplr 769 |
. . 3
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → 𝑦 = 𝑣) |
11 | | simpr 488 |
. . . . 5
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → 𝜑) |
12 | | sbequ1 2249 |
. . . . 5
⊢ (𝑦 = 𝑣 → (𝜑 → [𝑣 / 𝑦]𝜑)) |
13 | 10, 11, 12 | sylc 65 |
. . . 4
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → [𝑣 / 𝑦]𝜑) |
14 | | sbequ1 2249 |
. . . 4
⊢ (𝑥 = 𝑢 → ([𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
15 | 9, 13, 14 | sylc 65 |
. . 3
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) |
16 | 9, 10, 15 | jca31 518 |
. 2
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) |
17 | 8, 16 | impbii 212 |
1
⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)) |