Description: The implication between two sentences of propositional calculus is encoded by concatenating the two sentences and appending a two at the end. (Contributed by Thomas van Maaren, 21-Aug-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-propimp | |- prop-> = ( x e. _V , y e. _V |-> ( ( x ++ y ) ++ <" 2 "> ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cpropimp | |- prop-> |
|
| 1 | vx | |- x |
|
| 2 | cvv | |- _V |
|
| 3 | vy | |- y |
|
| 4 | 1 | cv | |- x |
| 5 | cconcat | |- ++ |
|
| 6 | 3 | cv | |- y |
| 7 | 4 6 5 | co | |- ( x ++ y ) |
| 8 | c2 | |- 2 |
|
| 9 | 8 | cs1 | |- <" 2 "> |
| 10 | 7 9 5 | co | |- ( ( x ++ y ) ++ <" 2 "> ) |
| 11 | 1 3 2 2 10 | cmpo | |- ( x e. _V , y e. _V |-> ( ( x ++ y ) ++ <" 2 "> ) ) |
| 12 | 0 11 | wceq | |- prop-> = ( x e. _V , y e. _V |-> ( ( x ++ y ) ++ <" 2 "> ) ) |