Theorem axc711to11

Description: Rederivation of ax-11 from axc711 . Note that ax-c7 and ax-11 are not used by the rederivation. (Contributed by NM, 18-Nov-2006) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		axc711toc7	|- ( -. 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		axc711	|- ( -. A. y -. A. x A. y ph -> A. x ph )
4	3	alimi	|- ( A. y -. A. y -. A. x A. y ph -> A. y A. x ph )
5	2 4	syl	|- ( A. x A. y ph -> A. y A. x ph )