Metamath Proof Explorer

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

Proof

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