Detailed syntax breakdown of Axiom ax-hvass
Step | Hyp | Ref
| Expression |
1 | | cA |
. . . 4
class 𝐴 |
2 | | chba 28866 |
. . . 4
class
ℋ |
3 | 1, 2 | wcel 2114 |
. . 3
wff 𝐴 ∈ ℋ |
4 | | cB |
. . . 4
class 𝐵 |
5 | 4, 2 | wcel 2114 |
. . 3
wff 𝐵 ∈ ℋ |
6 | | cC |
. . . 4
class 𝐶 |
7 | 6, 2 | wcel 2114 |
. . 3
wff 𝐶 ∈ ℋ |
8 | 3, 5, 7 | w3a 1088 |
. 2
wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈
ℋ) |
9 | | cva 28867 |
. . . . 5
class
+ℎ |
10 | 1, 4, 9 | co 7182 |
. . . 4
class (𝐴 +ℎ 𝐵) |
11 | 10, 6, 9 | co 7182 |
. . 3
class ((𝐴 +ℎ 𝐵) +ℎ 𝐶) |
12 | 4, 6, 9 | co 7182 |
. . . 4
class (𝐵 +ℎ 𝐶) |
13 | 1, 12, 9 | co 7182 |
. . 3
class (𝐴 +ℎ (𝐵 +ℎ 𝐶)) |
14 | 11, 13 | wceq 1542 |
. 2
wff ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶)) |
15 | 8, 14 | wi 4 |
1
wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵) +ℎ 𝐶) = (𝐴 +ℎ (𝐵 +ℎ 𝐶))) |