Axiom ax-sub 332

Description: Axiom of variable substitution.

Assertion

Ref	Expression
ax-sub	⊦ (x = y ⊸ (∀y𝜑 ⊸ ∀x(x = y ⊸ 𝜑)))

Detailed syntax breakdown of Axiom ax-sub

Step	Hyp	Ref	Expression
1		vx	. . . 4 var x
2	1	nvar 203	. . 3 nilad x
3		vy	. . . 4 var y
4	3	nvar 203	. . 3 nilad y
5	2, 4	weq 246	. 2 wff x = y
6		wph	. . . 4 wff 𝜑
7	6, 3	wal 318	. . 3 wff ∀y𝜑
8	5, 6	wli 61	. . . 4 wff (x = y ⊸ 𝜑)
9	8, 1	wal 318	. . 3 wff ∀x(x = y ⊸ 𝜑)
10	7, 9	wli 61	. 2 wff (∀y𝜑 ⊸ ∀x(x = y ⊸ 𝜑))
11	5, 10	wli 61	1 wff (x = y ⊸ (∀y𝜑 ⊸ ∀x(x = y ⊸ 𝜑)))

This axiom is referenced by: (None)