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 35899, ax-c7 35901, and ax-11 2151 in a subsystem that includes these axioms plus ax-c4 35900 and ax-gen 1787 (and propositional calculus). See axc5c711toc5 35935, axc5c711toc7 35936, and axc5c711to11 35937 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 35927. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
axc5c711 | ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-c5 35899 | . . 3 ⊢ (∀𝑦𝜑 → 𝜑) | |
2 | ax10fromc7 35911 | . . . 4 ⊢ (¬ ∀𝑦𝜑 → ∀𝑦 ¬ ∀𝑦𝜑) | |
3 | ax-c7 35901 | . . . . . 6 ⊢ (¬ ∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑦𝜑) | |
4 | 3 | con1i 149 | . . . . 5 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥 ¬ ∀𝑥∀𝑦𝜑) |
5 | 4 | alimi 1803 | . . . 4 ⊢ (∀𝑦 ¬ ∀𝑦𝜑 → ∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑) |
6 | ax-11 2151 | . . . 4 ⊢ (∀𝑦∀𝑥 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑) | |
7 | 2, 5, 6 | 3syl 18 | . . 3 ⊢ (¬ ∀𝑦𝜑 → ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑) |
8 | 1, 7 | nsyl4 161 | . 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → 𝜑) |
9 | ax-c5 35899 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
10 | 8, 9 | ja 187 | 1 ⊢ ((∀𝑥∀𝑦 ¬ ∀𝑥∀𝑦𝜑 → ∀𝑥𝜑) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ∀wal 1526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-11 2151 ax-c5 35899 ax-c4 35900 ax-c7 35901 |
This theorem is referenced by: axc5c711toc5 35935 axc5c711toc7 35936 axc5c711to11 35937 |
Copyright terms: Public domain | W3C validator |