Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ax12inda2ALT | Structured version Visualization version Unicode version |
Description: Alternate proof of ax12inda2 34232, slightly more direct and not requiring ax-c16 34177. (Contributed by NM, 4-May-2007.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
ax12inda2.1 |
Ref | Expression |
---|---|
ax12inda2ALT |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-1 6 | . . . . . . . 8 | |
2 | 1 | axc4i-o 34183 | . . . . . . 7 |
3 | 2 | a1i 11 | . . . . . 6 |
4 | biidd 252 | . . . . . . 7 | |
5 | 4 | dral1-o 34189 | . . . . . 6 |
6 | 5 | imbi2d 330 | . . . . . . 7 |
7 | 6 | dral2-o 34215 | . . . . . 6 |
8 | 3, 5, 7 | 3imtr4d 283 | . . . . 5 |
9 | 8 | aecoms-o 34187 | . . . 4 |
10 | 9 | a1d 25 | . . 3 |
11 | 10 | a1d 25 | . 2 |
12 | simplr 792 | . . . . 5 | |
13 | dveeq1-o 34220 | . . . . . . . 8 | |
14 | 13 | naecoms-o 34212 | . . . . . . 7 |
15 | 14 | imp 445 | . . . . . 6 |
16 | 15 | adantlr 751 | . . . . 5 |
17 | hbnae-o 34213 | . . . . . . 7 | |
18 | hba1-o 34182 | . . . . . . 7 | |
19 | 17, 18 | hban 2128 | . . . . . 6 |
20 | ax-c5 34168 | . . . . . . 7 | |
21 | ax12inda2.1 | . . . . . . . 8 | |
22 | 21 | imp 445 | . . . . . . 7 |
23 | 20, 22 | sylan2 491 | . . . . . 6 |
24 | 19, 23 | alimdh 1745 | . . . . 5 |
25 | 12, 16, 24 | syl2anc 693 | . . . 4 |
26 | ax-11 2034 | . . . . . 6 | |
27 | hbnae-o 34213 | . . . . . . 7 | |
28 | hbnae-o 34213 | . . . . . . . . 9 | |
29 | 28, 14 | nf5dh 2026 | . . . . . . . 8 |
30 | 19.21t 2073 | . . . . . . . 8 | |
31 | 29, 30 | syl 17 | . . . . . . 7 |
32 | 27, 31 | albidh 1793 | . . . . . 6 |
33 | 26, 32 | syl5ib 234 | . . . . 5 |
34 | 33 | ad2antrr 762 | . . . 4 |
35 | 25, 34 | syld 47 | . . 3 |
36 | 35 | exp31 630 | . 2 |
37 | 11, 36 | pm2.61i 176 | 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: (None) |
Copyright terms: Public domain | W3C validator |