Definition df-nre 244

Description: Definition of the dual read operator.

Assertion

Ref	Expression
df-nre	⊦ ([X ▷ y] 𝜑 ⧟ ~ [X ≫ y] ~ 𝜑)

Detailed syntax breakdown of Definition df-nre

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2		vy	. . 3 var y
3		nx	. . 3 nilad X
4	1, 2, 3	wnre 241	. 2 wff [X ▷ y] 𝜑
5	1	wneg 3	. . . 4 wff ~ 𝜑
6	5, 2, 3	wre 205	. . 3 wff [X ≫ y] ~ 𝜑
7	6	wneg 3	. 2 wff ~ [X ≫ y] ~ 𝜑
8	4, 7	wlb 55	1 wff ([X ▷ y] 𝜑 ⧟ ~ [X ≫ y] ~ 𝜑)

This definition is referenced by: (None)