Metamath Proof Explorer

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 ⊢ ∀ x ∀ y φ → ∀ y ∀ x φ

Proof

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