Description: Rederivation of Axiom ax-10 from ax-c7 , ax-c4 , ax-c5 , ax-gen and propositional calculus. See axc7 for the derivation of ax-c7 from ax-10 . (Contributed by NM, 23-May-2008) (Proof modification is discouraged.) Use ax-10 instead. (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ax10fromc7 | ⊢ ( ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 𝜑 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | ax-c4 | ⊢ ( ∀ 𝑥 ( ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 𝜑 → ¬ ∀ 𝑥 𝜑 ) → ( ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 𝜑 ) ) | |
| 2 | ax-c5 | ⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 𝜑 → ¬ ∀ 𝑥 ∀ 𝑥 𝜑 ) | |
| 3 | ax-c4 | ⊢ ( ∀ 𝑥 ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) → ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 𝜑 ) ) | |
| 4 | id | ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) | |
| 5 | 3 4 | mpg | ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 𝜑 ) |
| 6 | 2 5 | nsyl | ⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 𝜑 → ¬ ∀ 𝑥 𝜑 ) |
| 7 | 1 6 | mpg | ⊢ ( ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 𝜑 ) |
| 8 | ax-c7 | ⊢ ( ¬ ∀ 𝑥 ¬ ∀ 𝑥 ∀ 𝑥 𝜑 → ∀ 𝑥 𝜑 ) | |
| 9 | 7 8 | nsyl4 | ⊢ ( ¬ ∀ 𝑥 𝜑 → ∀ 𝑥 ¬ ∀ 𝑥 𝜑 ) |