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φ