"Are these equivalent?" Protoman, sci.logic

	1	ALL(x):[Human(x) => Mortal(x)]
		& EXIST(x):[Human(x) & Philosopher(x)]
		Premise

	2	ALL(x):[Human(x) => Mortal(x)]
		Split, 1

	3	EXIST(x):[Human(x) & Philosopher(x)]
		Split, 1

	4	Human(a) & Philosopher(a)
		E Spec, 3

	5	Human(a)
		Split, 4

	6	Philosopher(a)
		Split, 4

	7	Human(a) => Mortal(a)
		U Spec, 2

	8	Mortal(a)
		Detach, 7, 5

	9	Human(a) & Mortal(a)
		Join, 5, 8

	10	Human(a) & Mortal(a) & Philosopher(a)
		Join, 9, 6

	11	EXIST(x):[Human(x) & Mortal(x) & Philosopher(x)]
		E Gen, 10

12	ALL(x):[Human(x) => Mortal(x)]
	& EXIST(x):[Human(x) & Philosopher(x)]
	=> EXIST(x):[Human(x) & Mortal(x) & Philosopher(x)]
	Conclusion, 1