Mathbox for BJ |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > axc11n11r | Structured version Visualization version Unicode version |
Description: Proof of axc11n 2307 from { ax-1 6--
ax-7 1935, axc9 2302, axc11r 2187 } (note
that axc16 2135 is provable from { ax-1 6--
ax-7 1935, axc11r 2187 }).
Note that axc11n 2307 proves (over minimal calculus) that axc11 2314 and axc11r 2187 are equivalent. Therefore, axc11n11 32672 and axc11n11r 32673 prove that one can use one or the other as an axiom, provided one assumes the axioms listed above (axc11 2314 appears slightly stronger since axc11n11r 32673 requires axc9 2302 while axc11n11 32672 does not). (Contributed by BJ, 6-Jul-2021.) (Proof modification is discouraged.) |
Ref | Expression |
---|---|
axc11n11r |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equcomi 1944 | . . . . 5 | |
2 | axc16 2135 | . . . . 5 | |
3 | 1, 2 | syl5 34 | . . . 4 |
4 | 3 | spsd 2057 | . . 3 |
5 | 4 | exlimiv 1858 | . 2 |
6 | alnex 1706 | . . 3 | |
7 | ax6evr 1942 | . . . . 5 | |
8 | 19.29 1801 | . . . . 5 | |
9 | 7, 8 | mpan2 707 | . . . 4 |
10 | axc9 2302 | . . . . . . . . . . . 12 | |
11 | 10 | impcom 446 | . . . . . . . . . . 11 |
12 | axc11r 2187 | . . . . . . . . . . 11 | |
13 | 11, 12 | syl9 77 | . . . . . . . . . 10 |
14 | aev 1983 | . . . . . . . . . 10 | |
15 | 13, 14 | syl8 76 | . . . . . . . . 9 |
16 | 15 | ex 450 | . . . . . . . 8 |
17 | 16 | com24 95 | . . . . . . 7 |
18 | 17 | imp 445 | . . . . . 6 |
19 | pm2.18 122 | . . . . . 6 | |
20 | 18, 19 | syl6 35 | . . . . 5 |
21 | 20 | exlimiv 1858 | . . . 4 |
22 | 9, 21 | syl 17 | . . 3 |
23 | 6, 22 | sylbir 225 | . 2 |
24 | 5, 23 | pm2.61i 176 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wa 384 wal 1481 wex 1704 |
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-5 1839 ax-6 1888 ax-7 1935 ax-10 2019 ax-12 2047 ax-13 2246 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |