Mathbox for Andrew Salmon |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > axc11next | Structured version Visualization version Unicode version |
Description: This theorem shows that, given axext4 2606, we can derive a version of axc11n 2307. However, it is weaker than axc11n 2307 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
axc11next |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-ext 2602 | . . . . . 6 | |
2 | 1 | alimi 1739 | . . . . 5 |
3 | ax-11 2034 | . . . . . . 7 | |
4 | ax9 2003 | . . . . . . . . 9 | |
5 | biimpr 210 | . . . . . . . . . . 11 | |
6 | 5 | alimi 1739 | . . . . . . . . . 10 |
7 | stdpc5v 1867 | . . . . . . . . . 10 | |
8 | 6, 7 | syl 17 | . . . . . . . . 9 |
9 | 4, 8 | syl9 77 | . . . . . . . 8 |
10 | 9 | alimdv 1845 | . . . . . . 7 |
11 | 3, 10 | syl5 34 | . . . . . 6 |
12 | 11 | sps 2055 | . . . . 5 |
13 | 2, 12 | mpcom 38 | . . . 4 |
14 | 13 | axc4i 2131 | . . 3 |
15 | nfa1 2028 | . . . . . . . 8 | |
16 | 15 | 19.23 2080 | . . . . . . 7 |
17 | 19.8a 2052 | . . . . . . . . 9 | |
18 | elequ2 2004 | . . . . . . . . . 10 | |
19 | 18 | cbvexv 2275 | . . . . . . . . 9 |
20 | 17, 19 | sylib 208 | . . . . . . . 8 |
21 | 4 | cbvalivw 1934 | . . . . . . . 8 |
22 | 20, 21 | imim12i 62 | . . . . . . 7 |
23 | 16, 22 | sylbi 207 | . . . . . 6 |
24 | 23 | alimi 1739 | . . . . 5 |
25 | 24 | alcoms 2035 | . . . 4 |
26 | 25 | alrimiv 1855 | . . 3 |
27 | nfa1 2028 | . . . . . . . 8 | |
28 | 27 | 19.23 2080 | . . . . . . 7 |
29 | ax9 2003 | . . . . . . . . . 10 | |
30 | 29 | spimv 2257 | . . . . . . . . 9 |
31 | 17, 30 | imim12i 62 | . . . . . . . 8 |
32 | 19.8a 2052 | . . . . . . . . . 10 | |
33 | elequ2 2004 | . . . . . . . . . . 11 | |
34 | 33 | cbvexv 2275 | . . . . . . . . . 10 |
35 | 32, 34 | sylib 208 | . . . . . . . . 9 |
36 | sp 2053 | . . . . . . . . 9 | |
37 | 35, 36 | imim12i 62 | . . . . . . . 8 |
38 | 31, 37 | impbid 202 | . . . . . . 7 |
39 | 28, 38 | sylbi 207 | . . . . . 6 |
40 | 39 | alimi 1739 | . . . . 5 |
41 | 40 | alcoms 2035 | . . . 4 |
42 | 41 | axc4i 2131 | . . 3 |
43 | 14, 26, 42 | 3syl 18 | . 2 |
44 | axext4 2606 | . . 3 | |
45 | 44 | albii 1747 | . 2 |
46 | axext4 2606 | . . 3 | |
47 | 46 | albii 1747 | . 2 |
48 | 43, 45, 47 | 3imtr4i 281 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wal 1481 wceq 1483 wex 1704 wcel 1990 |
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-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-ex 1705 df-nf 1710 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |