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	⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		ax-1	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) )
2	1	alimi	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) )
3	2	axc4i	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) )
4	3	con3i	⊢ ( ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) → ¬ ∀ 𝑥 𝜑 )
5	4	alimi	⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) → ∀ 𝑥 ¬ ∀ 𝑥 𝜑 )
6	5	sps	⊢ ( ∀ 𝑥 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) → ∀ 𝑥 ¬ ∀ 𝑥 𝜑 )
7	6	con3i	⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → ¬ ∀ 𝑥 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) )
8		pm2.21	⊢ ( ¬ ∀ 𝑥 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) → ( ∀ 𝑥 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) → ( ( 𝜑 → 𝜑 ) → ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) ) ) )
9		axc5c4c711	⊢ ( ( ∀ 𝑥 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) → ( ( 𝜑 → 𝜑 ) → ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) ) ) → ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → ∀ 𝑥 𝜑 ) )
10	8 9	syl	⊢ ( ¬ ∀ 𝑥 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) → ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → ∀ 𝑥 𝜑 ) )
11		sp	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )
12	10 11	syl6	⊢ ( ¬ ∀ 𝑥 ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) → ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) )
13		pm2.27	⊢ ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → ( ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) → 𝜑 ) )
14		id	⊢ ( 𝜑 → 𝜑 )
15	13 14	mpg	⊢ ( ( ∀ 𝑥 ( 𝜑 → 𝜑 ) → 𝜑 ) → 𝜑 )
16	7 12 15	3syl	⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 𝜑 → 𝜑 )