Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > axc5c711 | Structured version Visualization version Unicode version |
Description: Proof of a single axiom that can replace ax-c5 34168, ax-c7 34170, and ax-11 2034 in a subsystem that includes these axioms plus ax-c4 34169 and ax-gen 1722 (and propositional calculus). See axc5c711toc5 34204, axc5c711toc7 34205, and axc5c711to11 34206 for the rederivation of those axioms. This theorem extends the idea in Scott Fenton's axc5c7 34196. (Contributed by NM, 18-Nov-2006.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
axc5c711 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-c5 34168 | . . 3 | |
2 | ax10fromc7 34180 | . . . 4 | |
3 | ax-c7 34170 | . . . . . 6 | |
4 | 3 | con1i 144 | . . . . 5 |
5 | 4 | alimi 1739 | . . . 4 |
6 | ax-11 2034 | . . . 4 | |
7 | 2, 5, 6 | 3syl 18 | . . 3 |
8 | 1, 7 | nsyl4 156 | . 2 |
9 | ax-c5 34168 | . 2 | |
10 | 8, 9 | ja 173 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wal 1481 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-11 2034 ax-c5 34168 ax-c4 34169 ax-c7 34170 |
This theorem is referenced by: axc5c711toc5 34204 axc5c711toc7 34205 axc5c711to11 34206 |
Copyright terms: Public domain | W3C validator |