Theorem axc5c711to11

Description: Rederivation of ax-11 from axc5c711 . Note that ax-c7 and ax-11 are not used by the rederivation. The use of alimi (which uses ax-c5 ) is allowed since we have already proved axc5c711toc5 . (Contributed by NM, 19-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	axc5c711to11	|- ( A. x A. y ph -> A. y A. x ph )

Proof

Step	Hyp	Ref	Expression
1		axc5c711toc7	|- ( -. A. y -. A. y -. A. x A. y ph -> -. A. x A. y ph )
2	1	con4i	|- ( A. x A. y ph -> A. y -. A. y -. A. x A. y ph )
3		pm2.21	|- ( -. A. x A. y -. A. x A. y ph -> ( A. x A. y -. A. x A. y ph -> A. x ph ) )
4		axc5c711	|- ( ( A. x A. y -. A. x A. y ph -> A. x ph ) -> ph )
5	3 4	syl	|- ( -. A. x A. y -. A. x A. y ph -> ph )
6	5	alimi	|- ( A. x -. A. x A. y -. A. x A. y ph -> A. x ph )
7		axc5c711toc7	|- ( -. A. x -. A. x A. y -. A. x A. y ph -> A. y -. A. x A. y ph )
8	6 7	nsyl4	|- ( -. A. y -. A. x A. y ph -> A. x ph )
9	8	alimi	|- ( A. y -. A. y -. A. x A. y ph -> A. y A. x ph )
10	2 9	syl	|- ( A. x A. y ph -> A. y A. x ph )