Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax12indalem | Structured version Visualization version Unicode version |
Description: Lemma for ax12inda2 34232 and ax12inda 34233. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax12indalem.1 |
Ref | Expression |
---|---|
ax12indalem |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1 6 | . . . . . . . . 9 | |
2 | 1 | axc4i-o 34183 | . . . . . . . 8 |
3 | 2 | a1i 11 | . . . . . . 7 |
4 | biidd 252 | . . . . . . . 8 | |
5 | 4 | dral1-o 34189 | . . . . . . 7 |
6 | 5 | imbi2d 330 | . . . . . . . 8 |
7 | 6 | dral2-o 34215 | . . . . . . 7 |
8 | 3, 5, 7 | 3imtr4d 283 | . . . . . 6 |
9 | 8 | aecoms-o 34187 | . . . . 5 |
10 | 9 | a1d 25 | . . . 4 |
11 | 10 | a1d 25 | . . 3 |
12 | 11 | adantr 481 | . 2 |
13 | simplr 792 | . . . . 5 | |
14 | aecom-o 34186 | . . . . . . . . 9 | |
15 | 14 | con3i 150 | . . . . . . . 8 |
16 | aecom-o 34186 | . . . . . . . . 9 | |
17 | 16 | con3i 150 | . . . . . . . 8 |
18 | axc9 2302 | . . . . . . . . 9 | |
19 | 18 | imp 445 | . . . . . . . 8 |
20 | 15, 17, 19 | syl2an 494 | . . . . . . 7 |
21 | 20 | imp 445 | . . . . . 6 |
22 | 21 | adantlr 751 | . . . . 5 |
23 | hbnae-o 34213 | . . . . . . 7 | |
24 | hba1-o 34182 | . . . . . . 7 | |
25 | 23, 24 | hban 2128 | . . . . . 6 |
26 | ax-c5 34168 | . . . . . . 7 | |
27 | ax12indalem.1 | . . . . . . . 8 | |
28 | 27 | imp 445 | . . . . . . 7 |
29 | 26, 28 | sylan2 491 | . . . . . 6 |
30 | 25, 29 | alimdh 1745 | . . . . 5 |
31 | 13, 22, 30 | syl2anc 693 | . . . 4 |
32 | ax-11 2034 | . . . . . 6 | |
33 | hbnae-o 34213 | . . . . . . . 8 | |
34 | hbnae-o 34213 | . . . . . . . 8 | |
35 | 33, 34 | hban 2128 | . . . . . . 7 |
36 | hbnae-o 34213 | . . . . . . . . . 10 | |
37 | hbnae-o 34213 | . . . . . . . . . 10 | |
38 | 36, 37 | hban 2128 | . . . . . . . . 9 |
39 | 38, 20 | nf5dh 2026 | . . . . . . . 8 |
40 | 19.21t 2073 | . . . . . . . 8 | |
41 | 39, 40 | syl 17 | . . . . . . 7 |
42 | 35, 41 | albidh 1793 | . . . . . 6 |
43 | 32, 42 | syl5ib 234 | . . . . 5 |
44 | 43 | ad2antrr 762 | . . . 4 |
45 | 31, 44 | syld 47 | . . 3 |
46 | 45 | exp31 630 | . 2 |
47 | 12, 46 | pm2.61ian 831 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wb 196 wa 384 wal 1481 wnf 1708 |
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-11 2034 ax-12 2047 ax-13 2246 ax-c5 34168 ax-c4 34169 ax-c7 34170 ax-c10 34171 ax-c11 34172 ax-c9 34175 |
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: ax12inda2 34232 |
Copyright terms: Public domain | W3C validator |