Reversibility of Universal Quantifiers

Comments (in blue font)
********

Prove: Ax Ay [P(x) & Q(y) -> R(x,y)] -> Ay Ax [P(x) & Q(y) -> R(x,y)]

Or, in the DC Proof notation...

Prove: ALL(x):ALL(y):[P(x) & Q(y) => R(x,y)]=> ALL(y):ALL(x):[P(x) & Q(y) => R(x,y)]

	
	Proof
	*****
	
	Suppose...

	1	ALL(x):ALL(y):[P(x) & Q(y) => R(x,y)]
		Premise

		
		Prove: P(s) & Q(t) => R(s,t) for arbitrary s and t
		
		Suppose...

		2	P(s) & Q(t)
			Premise

		3	ALL(y):[P(s) & Q(y) => R(s,y)]
			U Spec, 1

		4	P(s) & Q(t) => R(s,t)
			U Spec, 3

		5	R(s,t)
			Detach, 4, 2

	As Required:

	6	P(s) & Q(t) => R(s,t)
		Conclusion, 2
	Generalizing...

	7	ALL(x):[P(x) & Q(t) => R(x,t)]
		U Gen, 6

	8	ALL(y):ALL(x):[P(x) & Q(y) => R(x,y)]
		U Gen, 7

As Required:

9	ALL(x):ALL(y):[P(x) & Q(y) => R(x,y)]
	=> ALL(y):ALL(x):[P(x) & Q(y) => R(x,y)]
	Conclusion, 1