Axiom ax-subre1 223

Assertion

Ref	Expression
ax-subre1	⊦ ([x ≔ y] [x ≫ a] 𝜑 ⧟ [x ≔ y] [y ≫ a] 𝜑)

Detailed syntax breakdown of Axiom ax-subre1

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		va	. . . 4 var a
3		vx	. . . . 5 var x
4	3	nvar 203	. . . 4 nilad x
5	1, 2, 4	wre 205	. . 3 wff [x ≫ a] 𝜑
6		vy	. . . 4 var y
7	6	nvar 203	. . 3 nilad y
8	5, 3, 7	wsub 207	. 2 wff [x ≔ y] [x ≫ a] 𝜑
9	1, 2, 7	wre 205	. . 3 wff [y ≫ a] 𝜑
10	9, 3, 7	wsub 207	. 2 wff [x ≔ y] [y ≫ a] 𝜑
11	8, 10	wlb 55	1 wff ([x ≔ y] [x ≫ a] 𝜑 ⧟ [x ≔ y] [y ≫ a] 𝜑)

This axiom is referenced by: (None)