Detailed syntax breakdown of Axiom ax-his2
| Step | Hyp | Ref
| Expression |
| 1 | | cA |
. . . 4
class 𝐴 |
| 2 | | chba 30938 |
. . . 4
class
ℋ |
| 3 | 1, 2 | wcel 2108 |
. . 3
wff 𝐴 ∈ ℋ |
| 4 | | cB |
. . . 4
class 𝐵 |
| 5 | 4, 2 | wcel 2108 |
. . 3
wff 𝐵 ∈ ℋ |
| 6 | | cC |
. . . 4
class 𝐶 |
| 7 | 6, 2 | wcel 2108 |
. . 3
wff 𝐶 ∈ ℋ |
| 8 | 3, 5, 7 | w3a 1087 |
. 2
wff (𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈
ℋ) |
| 9 | | cva 30939 |
. . . . 5
class
+ℎ |
| 10 | 1, 4, 9 | co 7431 |
. . . 4
class (𝐴 +ℎ 𝐵) |
| 11 | | csp 30941 |
. . . 4
class
·ih |
| 12 | 10, 6, 11 | co 7431 |
. . 3
class ((𝐴 +ℎ 𝐵)
·ih 𝐶) |
| 13 | 1, 6, 11 | co 7431 |
. . . 4
class (𝐴
·ih 𝐶) |
| 14 | 4, 6, 11 | co 7431 |
. . . 4
class (𝐵
·ih 𝐶) |
| 15 | | caddc 11158 |
. . . 4
class
+ |
| 16 | 13, 14, 15 | co 7431 |
. . 3
class ((𝐴
·ih 𝐶) + (𝐵 ·ih 𝐶)) |
| 17 | 12, 16 | wceq 1540 |
. 2
wff ((𝐴 +ℎ 𝐵)
·ih 𝐶) = ((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐶)) |
| 18 | 8, 17 | wi 4 |
1
wff ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ) → ((𝐴 +ℎ 𝐵)
·ih 𝐶) = ((𝐴 ·ih 𝐶) + (𝐵 ·ih 𝐶))) |