Axiom ax-subre2 224

Assertion

Ref	Expression
ax-subre2	⊦ ([x ≔ y] [u ≫ v] 𝜑 ⧟ [u ≫ v] [x ≔ y] 𝜑)

Distinct variable groups:   u,x   u,y   v,x   v,y

Detailed syntax breakdown of Axiom ax-subre2

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

This axiom is referenced by: (None)