Theorem axc5c4c711toc7

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

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

Proof

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