Theorem impprop

Description: The implication between two sentences of propositional calculus is a sentence of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

	Ref	Expression
Assertion	impprop	Could not format assertion : No typesetting found for |- ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. PROP ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-prop	Could not format PROP = setrecs ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ) : No typesetting found for |- PROP = setrecs ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ) with typecode |-
2		prex	$$⊢\left\{x,y\right\}\in \mathrm{V}$$
3	2	a1i	Could not format ( ( x e. PROP /\ y e. PROP ) -> { x , y } e. _V ) : No typesetting found for |- ( ( x e. PROP /\ y e. PROP ) -> { x , y } e. _V ) with typecode |-
4		prssi	Could not format ( ( x e. PROP /\ y e. PROP ) -> { x , y } C_ PROP ) : No typesetting found for |- ( ( x e. PROP /\ y e. PROP ) -> { x , y } C_ PROP ) with typecode |-
5	1 3 4	setrec1	Could not format ( ( x e. PROP /\ y e. PROP ) -> ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) C_ PROP ) : No typesetting found for |- ( ( x e. PROP /\ y e. PROP ) -> ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) C_ PROP ) with typecode |-
6		vex	$$⊢y\in \mathrm{V}$$
7		vex	$$⊢x\in \mathrm{V}$$
8		oveq2	Could not format ( v = y -> ( u prop-> v ) = ( u prop-> y ) ) : No typesetting found for |- ( v = y -> ( u prop-> v ) = ( u prop-> y ) ) with typecode |-
9	8	eqeq2d	Could not format ( v = y -> ( z = ( u prop-> v ) <-> z = ( u prop-> y ) ) ) : No typesetting found for |- ( v = y -> ( z = ( u prop-> v ) <-> z = ( u prop-> y ) ) ) with typecode |-
10		oveq1	Could not format ( u = x -> ( u prop-> y ) = ( x prop-> y ) ) : No typesetting found for |- ( u = x -> ( u prop-> y ) = ( x prop-> y ) ) with typecode |-
11	10	eqeq2d	Could not format ( u = x -> ( z = ( u prop-> y ) <-> z = ( x prop-> y ) ) ) : No typesetting found for |- ( u = x -> ( z = ( u prop-> y ) <-> z = ( x prop-> y ) ) ) with typecode |-
12	6 7 9 11	ceqsex2v	Could not format ( E. v E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> z = ( x prop-> y ) ) : No typesetting found for |- ( E. v E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> z = ( x prop-> y ) ) with typecode |-
13	12	bilanri	Could not format ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) ) : No typesetting found for |- ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) ) with typecode |-
14		3anass	Could not format ( ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> ( v = y /\ ( u = x /\ z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> ( v = y /\ ( u = x /\ z = ( u prop-> v ) ) ) ) with typecode |-
15	14	exbii	Could not format ( E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> E. u ( v = y /\ ( u = x /\ z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> E. u ( v = y /\ ( u = x /\ z = ( u prop-> v ) ) ) ) with typecode |-
16		19.42v	Could not format ( E. u ( v = y /\ ( u = x /\ z = ( u prop-> v ) ) ) <-> ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( E. u ( v = y /\ ( u = x /\ z = ( u prop-> v ) ) ) <-> ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) ) with typecode |-
17	15 16	bitri	Could not format ( E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) ) with typecode |-
18	17	exbii	Could not format ( E. v E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> E. v ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( E. v E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> E. v ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) ) with typecode |-
19	13 18	sylib	Could not format ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) ) with typecode |-
20		olc	$$⊢v=y\to \left(v=x\vee v=y\right)$$
21		vex	$$⊢v\in \mathrm{V}$$
22	21	elpr	$$⊢v\in \left\{x,y\right\}\leftrightarrow \left(v=x\vee v=y\right)$$
23	20 22	sylibr	$$⊢v=y\to v\in \left\{x,y\right\}$$
24		orc	$$⊢u=x\to \left(u=x\vee u=y\right)$$
25		vex	$$⊢u\in \mathrm{V}$$
26	25	elpr	$$⊢u\in \left\{x,y\right\}\leftrightarrow \left(u=x\vee u=y\right)$$
27	24 26	sylibr	$$⊢u=x\to u\in \left\{x,y\right\}$$
28	27	anim1i	Could not format ( ( u = x /\ z = ( u prop-> v ) ) -> ( u e. { x , y } /\ z = ( u prop-> v ) ) ) : No typesetting found for |- ( ( u = x /\ z = ( u prop-> v ) ) -> ( u e. { x , y } /\ z = ( u prop-> v ) ) ) with typecode |-
29	28	eximi	Could not format ( E. u ( u = x /\ z = ( u prop-> v ) ) -> E. u ( u e. { x , y } /\ z = ( u prop-> v ) ) ) : No typesetting found for |- ( E. u ( u = x /\ z = ( u prop-> v ) ) -> E. u ( u e. { x , y } /\ z = ( u prop-> v ) ) ) with typecode |-
30		df-rex	Could not format ( E. u e. { x , y } z = ( u prop-> v ) <-> E. u ( u e. { x , y } /\ z = ( u prop-> v ) ) ) : No typesetting found for |- ( E. u e. { x , y } z = ( u prop-> v ) <-> E. u ( u e. { x , y } /\ z = ( u prop-> v ) ) ) with typecode |-
31	29 30	sylibr	Could not format ( E. u ( u = x /\ z = ( u prop-> v ) ) -> E. u e. { x , y } z = ( u prop-> v ) ) : No typesetting found for |- ( E. u ( u = x /\ z = ( u prop-> v ) ) -> E. u e. { x , y } z = ( u prop-> v ) ) with typecode |-
32	31	olcd	Could not format ( E. u ( u = x /\ z = ( u prop-> v ) ) -> ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) : No typesetting found for |- ( E. u ( u = x /\ z = ( u prop-> v ) ) -> ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) with typecode |-
33	23 32	anim12i	Could not format ( ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) -> ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) -> ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) with typecode |-
34	33	eximi	Could not format ( E. v ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) -> E. v ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( E. v ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) -> E. v ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) with typecode |-
35	19 34	syl	Could not format ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) with typecode |-
36		df-rex	Could not format ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) <-> E. v ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) <-> E. v ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) with typecode |-
37	35 36	sylibr	Could not format ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) : No typesetting found for |- ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) with typecode |-
38	37	orcd	Could not format ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) : No typesetting found for |- ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) with typecode |-
39	38	ex	Could not format ( ( x e. PROP /\ y e. PROP ) -> ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) : No typesetting found for |- ( ( x e. PROP /\ y e. PROP ) -> ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) with typecode |-
40	39	alrimiv	Could not format ( ( x e. PROP /\ y e. PROP ) -> A. z ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) : No typesetting found for |- ( ( x e. PROP /\ y e. PROP ) -> A. z ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) with typecode |-
41		ovex	Could not format ( x prop-> y ) e. _V : No typesetting found for |- ( x prop-> y ) e. _V with typecode |-
42		elab6g	Could not format ( ( x prop-> y ) e. _V -> ( ( x prop-> y ) e. { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } <-> A. z ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) ) : No typesetting found for |- ( ( x prop-> y ) e. _V -> ( ( x prop-> y ) e. { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } <-> A. z ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) ) with typecode |-
43	41 42	ax-mp	Could not format ( ( x prop-> y ) e. { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } <-> A. z ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) : No typesetting found for |- ( ( x prop-> y ) e. { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } <-> A. z ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) with typecode |-
44	40 43	sylibr	Could not format ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) : No typesetting found for |- ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) with typecode |-
45		rexeq	Could not format ( w = { x , y } -> ( E. u e. w z = ( u prop-> v ) <-> E. u e. { x , y } z = ( u prop-> v ) ) ) : No typesetting found for |- ( w = { x , y } -> ( E. u e. w z = ( u prop-> v ) <-> E. u e. { x , y } z = ( u prop-> v ) ) ) with typecode |-
46	45	orbi2d	Could not format ( w = { x , y } -> ( ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) <-> ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( w = { x , y } -> ( ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) <-> ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) with typecode |-
47	46	rexeqbi1dv	Could not format ( w = { x , y } -> ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) <-> E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) : No typesetting found for |- ( w = { x , y } -> ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) <-> E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) ) with typecode |-
48	47	orbi1d	Could not format ( w = { x , y } -> ( ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) <-> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) : No typesetting found for |- ( w = { x , y } -> ( ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) <-> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) with typecode |-
49	48	abbidv	Could not format ( w = { x , y } -> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } = { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) : No typesetting found for |- ( w = { x , y } -> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } = { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) with typecode |-
50		eqid	Could not format ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) = ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) : No typesetting found for |- ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) = ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) with typecode |-
51	2	dfproplem	Could not format { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } e. _V : No typesetting found for |- { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } e. _V with typecode |-
52	49 50 51	fvmpt	Could not format ( { x , y } e. _V -> ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) = { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) : No typesetting found for |- ( { x , y } e. _V -> ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) = { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) with typecode |-
53	2 52	ax-mp	Could not format ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) = { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } : No typesetting found for |- ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) = { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } with typecode |-
54	44 53	eleqtrrdi	Could not format ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) ) : No typesetting found for |- ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) ) with typecode |-
55	5 54	sseldd	Could not format ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. PROP ) : No typesetting found for |- ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. PROP ) with typecode |-