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 φ → φ