Axiom ax-send 228

Description: Message passing.

Assertion

Ref	Expression
ax-send	⊦ (([z ≪ y] 𝜑 ⊗ [z ≫ x] 𝜓) ⊸ (𝜑 ⊗ [x ≔ y] 𝜓))

Detailed syntax breakdown of Axiom ax-send

Step	Hyp	Ref	Expression
1		wph	. . . 4 wff 𝜑
2		vz	. . . . 5 var z
3	2	nvar 203	. . . 4 nilad z
4		vy	. . . . 5 var y
5	4	nvar 203	. . . 4 nilad y
6	1, 3, 5	wse 204	. . 3 wff [z ≪ y] 𝜑
7		wps	. . . 4 wff 𝜓
8		vx	. . . 4 var x
9	7, 8, 3	wre 205	. . 3 wff [z ≫ x] 𝜓
10	6, 9	wmc 105	. 2 wff ([z ≪ y] 𝜑 ⊗ [z ≫ x] 𝜓)
11	7, 8, 5	wsub 207	. . 3 wff [x ≔ y] 𝜓
12	1, 11	wmc 105	. 2 wff (𝜑 ⊗ [x ≔ y] 𝜓)
13	10, 12	wli 61	1 wff (([z ≪ y] 𝜑 ⊗ [z ≫ x] 𝜓) ⊸ (𝜑 ⊗ [x ≔ y] 𝜓))

This axiom is referenced by: (None)