Mathbox for Alan Sare |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > vk15.4j | Structured version Visualization version Unicode version |
Description: Excercise 4j of Unit 15 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. This proof is the minimized Hilbert-style axiomatic version of the Fitch-style Natural Deduction proof found on page 442 of Klenk and was automatically derived from that proof. vk15.4j 38734 is vk15.4jVD 39150 automatically translated and minimized. (Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Ref | Expression |
---|---|
vk15.4j.1 | |
vk15.4j.2 | |
vk15.4j.3 |
Ref | Expression |
---|---|
vk15.4j |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vk15.4j.3 | . . . . . 6 | |
2 | exanali 1786 | . . . . . 6 | |
3 | 1, 2 | mpbir 221 | . . . . 5 |
4 | vk15.4j.2 | . . . . . 6 | |
5 | alex 1753 | . . . . . . . . . 10 | |
6 | 5 | biimpri 218 | . . . . . . . . 9 |
7 | 6 | 19.21bi 2059 | . . . . . . . 8 |
8 | simpl 473 | . . . . . . . . 9 | |
9 | 8 | a1i 11 | . . . . . . . 8 |
10 | 19.8a 2052 | . . . . . . . 8 | |
11 | 7, 9, 10 | syl6an 568 | . . . . . . 7 |
12 | notnot 136 | . . . . . . 7 | |
13 | 11, 12 | syl6 35 | . . . . . 6 |
14 | con3 149 | . . . . . 6 | |
15 | 4, 13, 14 | mpsylsyld 69 | . . . . 5 |
16 | hbe1 2021 | . . . . . 6 | |
17 | 16 | hbn 2146 | . . . . 5 |
18 | hbn1 2020 | . . . . 5 | |
19 | 3, 15, 17, 18 | eexinst01 38732 | . . . 4 |
20 | exnal 1754 | . . . 4 | |
21 | 19, 20 | sylibr 224 | . . 3 |
22 | vk15.4j.1 | . . . . . . . . 9 | |
23 | pm3.13 522 | . . . . . . . . 9 | |
24 | 22, 23 | ax-mp 5 | . . . . . . . 8 |
25 | simpr 477 | . . . . . . . . . . . 12 | |
26 | 25 | a1i 11 | . . . . . . . . . . 11 |
27 | 19.8a 2052 | . . . . . . . . . . 11 | |
28 | 26, 27 | syl6 35 | . . . . . . . . . 10 |
29 | hbe1 2021 | . . . . . . . . . 10 | |
30 | 3, 28, 17, 29 | eexinst01 38732 | . . . . . . . . 9 |
31 | notnot 136 | . . . . . . . . 9 | |
32 | 30, 31 | syl 17 | . . . . . . . 8 |
33 | pm2.53 388 | . . . . . . . 8 | |
34 | 24, 32, 33 | mpsyl 68 | . . . . . . 7 |
35 | exanali 1786 | . . . . . . . 8 | |
36 | 35 | con5i 38729 | . . . . . . 7 |
37 | 34, 36 | syl 17 | . . . . . 6 |
38 | 37 | 19.21bi 2059 | . . . . 5 |
39 | 38 | con3d 148 | . . . 4 |
40 | 19.8a 2052 | . . . 4 | |
41 | 39, 40 | syl6 35 | . . 3 |
42 | hbe1 2021 | . . 3 | |
43 | 21, 41, 17, 42 | eexinst11 38733 | . 2 |
44 | exnal 1754 | . 2 | |
45 | 43, 44 | sylib 208 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wn 3 wi 4 wo 383 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 |
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 |