![]() |
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 34691, ax-c7 34693, and ax-11 2190 in a subsystem that includes these axioms plus ax-c4 34692 and ax-gen 1870 (and propositional calculus). See axc5c711toc5 34727, axc5c711toc7 34728, and axc5c711to11 34729 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 34719. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
axc5c711 | ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-c5 34691 | . . 3 ⊢ (∀𝑦𝜑 → 𝜑) | |
2 | ax10fromc7 34703 | . . . 4 ⊢ (¬ ∀𝑦𝜑 → ∀𝑦 ¬ ∀𝑦𝜑) | |
3 | ax-c7 34693 | . . . . . 6 ⊢ (¬ ∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑦𝜑) | |
4 | 3 | con1i 146 | . . . . 5 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥 ¬ ∀𝑥∀𝑦𝜑) |
5 | 4 | alimi 1887 | . . . 4 ⊢ (∀𝑦 ¬ ∀𝑦𝜑 → ∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑) |
6 | ax-11 2190 | . . . 4 ⊢ (∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑) | |
7 | 2, 5, 6 | 3syl 18 | . . 3 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑) |
8 | 1, 7 | nsyl4 157 | . 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → 𝜑) |
9 | ax-c5 34691 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
10 | 8, 9 | ja 174 | 1 ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1629 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-11 2190 ax-c5 34691 ax-c4 34692 ax-c7 34693 |
This theorem is referenced by: axc5c711toc5 34727 axc5c711toc7 34728 axc5c711to11 34729 |
Copyright terms: Public domain | W3C validator |