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

Proof

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