Theorem axc5c4c711to11

Description: Rederivation of ax-11 from axc5c4c711 . Note that ax-11 is not required for the rederivation. (Contributed by Andrew Salmon, 14-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax-1	|- ( ph -> ( A. y ( ph -> ph ) -> ph ) )
2	1	2alimi	|- ( A. x A. y ph -> A. x A. y ( A. y ( ph -> ph ) -> ph ) )
3		axc5c4c711toc7	|- ( -. A. y -. A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) -> -. A. x A. y ( A. y ( ph -> ph ) -> ph ) )
4	3	con4i	|- ( A. x A. y ( A. y ( ph -> ph ) -> ph ) -> A. y -. A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) )
5		pm2.21	|- ( -. A. x A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) -> ( A. x A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) -> ( ( ph -> ph ) -> A. y ( A. y ( ph -> ph ) -> ph ) ) ) )
6		axc5c4c711	|- ( ( A. x A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) -> ( ( ph -> ph ) -> A. y ( A. y ( ph -> ph ) -> ph ) ) ) -> ( A. y ( ph -> ph ) -> A. y ph ) )
7		sp	|- ( A. y ph -> ph )
8	6 7	syl6	|- ( ( A. x A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) -> ( ( ph -> ph ) -> A. y ( A. y ( ph -> ph ) -> ph ) ) ) -> ( A. y ( ph -> ph ) -> ph ) )
9	5 8	syl	|- ( -. A. x A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) -> ( A. y ( ph -> ph ) -> ph ) )
10	9	alimi	|- ( A. x -. A. x A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) -> A. x ( A. y ( ph -> ph ) -> ph ) )
11		axc5c4c711toc7	|- ( -. A. x -. A. x A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) -> A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) )
12	10 11	nsyl4	|- ( -. A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) -> A. x ( A. y ( ph -> ph ) -> ph ) )
13	12	alimi	|- ( A. y -. A. y -. A. x A. y ( A. y ( ph -> ph ) -> ph ) -> A. y A. x ( A. y ( ph -> ph ) -> ph ) )
14	4 13	syl	|- ( A. x A. y ( A. y ( ph -> ph ) -> ph ) -> A. y A. x ( A. y ( ph -> ph ) -> ph ) )
15		pm2.27	|- ( A. y ( ph -> ph ) -> ( ( A. y ( ph -> ph ) -> ph ) -> ph ) )
16		id	|- ( ph -> ph )
17	15 16	mpg	|- ( ( A. y ( ph -> ph ) -> ph ) -> ph )
18	17	2alimi	|- ( A. y A. x ( A. y ( ph -> ph ) -> ph ) -> A. y A. x ph )
19	2 14 18	3syl	|- ( A. x A. y ph -> A. y A. x ph )