Detailed syntax breakdown of Axiom ax-newstateeq
Step | Hyp | Ref
| Expression |
1 | | wva |
. . . . 5
term a |
2 | | wvb |
. . . . 5
term b |
3 | 1, 2 | wi1 12 |
. . . 4
term (a →1 b) |
4 | | wvc |
. . . . 5
term c |
5 | 4, 2 | wi1 12 |
. . . 4
term (c →1 b) |
6 | 3, 5 | wi1 12 |
. . 3
term ((a →1 b) →1 (c →1 b)) |
7 | 1, 4 | wi1 12 |
. . . 4
term (a →1 c) |
8 | 2, 1 | wi1 12 |
. . . 4
term (b →1 a) |
9 | 7, 8 | wa 7 |
. . 3
term ((a →1 c) ∩ (b
→1 a)) |
10 | 6, 9 | wa 7 |
. 2
term (((a →1 b) →1 (c →1 b)) ∩ ((a
→1 c) ∩ (b →1 a))) |
11 | 4, 1 | wi1 12 |
. 2
term (c →1 a) |
12 | 10, 11 | wle 2 |
1
wff (((a →1 b) →1 (c →1 b)) ∩ ((a
→1 c) ∩ (b →1 a))) ≤ (c
→1 a) |