Definition df-propimp

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	Could not format assertion : No typesetting found for |- prop-> = ( x e. _V , y e. _V |-> ( ( x ++ y ) ++ <" 2 "> ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cpropimp	Could not format prop-> : No typesetting found for class prop-> with typecode class
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		vy	$$setvary$$
4	1	cv	$$setvarx$$
5		cconcat	$$class\mathrm{++}$$
6	3	cv	$$setvary$$
7	4 6 5	co	$$class\left(x\mathrm{++}y\right)$$
8		c2	$$class2$$
9	8	cs1	$$class⟨“2”⟩$$
10	7 9 5	co	$$class\left(\left(x\mathrm{++}y\right)\mathrm{++}⟨“2”⟩\right)$$
11	1 3 2 2 10	cmpo	$$class\left(x\in \mathrm{V},y\in \mathrm{V}⟼\left(x\mathrm{++}y\right)\mathrm{++}⟨“2”⟩\right)$$
12	0 11	wceq	Could not format prop-> = ( x e. _V , y e. _V |-> ( ( x ++ y ) ++ <" 2 "> ) ) : No typesetting found for wff prop-> = ( x e. _V , y e. _V |-> ( ( x ++ y ) ++ <" 2 "> ) ) with typecode wff