Axiom ax-7d

Description: Distinct variable version of ax-11 . (Contributed by Mario Carneiro, 14-Aug-2015)

	Ref	Expression
Assertion	ax-7d	|- ( A. x A. y ph -> A. y A. x ph )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	|- x
1		vy	|- y
2		wph	|- ph
3	2 1	wal	|- A. y ph
4	3 0	wal	|- A. x A. y ph
5	2 0	wal	|- A. x ph
6	5 1	wal	|- A. y A. x ph
7	4 6	wi	|- ( A. x A. y ph -> A. y A. x ph )