![]() |
Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > axc5c711 | Structured version Visualization version GIF version |
Description: Proof of a single axiom that can replace ax-c5 37742, ax-c7 37744, and ax-11 2155 in a subsystem that includes these axioms plus ax-c4 37743 and ax-gen 1798 (and propositional calculus). See axc5c711toc5 37778, axc5c711toc7 37779, and axc5c711to11 37780 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 37770. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
axc5c711 | ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-c5 37742 | . . 3 ⊢ (∀𝑦𝜑 → 𝜑) | |
2 | ax10fromc7 37754 | . . . 4 ⊢ (¬ ∀𝑦𝜑 → ∀𝑦 ¬ ∀𝑦𝜑) | |
3 | ax-c7 37744 | . . . . . 6 ⊢ (¬ ∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑦𝜑) | |
4 | 3 | con1i 147 | . . . . 5 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥 ¬ ∀𝑥∀𝑦𝜑) |
5 | 4 | alimi 1814 | . . . 4 ⊢ (∀𝑦 ¬ ∀𝑦𝜑 → ∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑) |
6 | ax-11 2155 | . . . 4 ⊢ (∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑) | |
7 | 2, 5, 6 | 3syl 18 | . . 3 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑) |
8 | 1, 7 | nsyl4 158 | . 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → 𝜑) |
9 | ax-c5 37742 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
10 | 8, 9 | ja 186 | 1 ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1540 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-11 2155 ax-c5 37742 ax-c4 37743 ax-c7 37744 |
This theorem is referenced by: axc5c711toc5 37778 axc5c711toc7 37779 axc5c711to11 37780 |
Copyright terms: Public domain | W3C validator |