Proof of Theorem ax3
Step | Hyp | Ref
| Expression |
1 | | ax3.1 |
. . . . 5
⊢ R:∗ |
2 | | wnot 128 |
. . . . . 6
⊢ ¬ :(∗
→ ∗) |
3 | 2, 1 | wc 45 |
. . . . 5
⊢ (¬ R):∗ |
4 | | wim 127 |
. . . . . . . 8
⊢ ⇒ :(∗
→ (∗ → ∗)) |
5 | | ax3.2 |
. . . . . . . . 9
⊢ S:∗ |
6 | 2, 5 | wc 45 |
. . . . . . . 8
⊢ (¬ S):∗ |
7 | 4, 3, 6 | wov 64 |
. . . . . . 7
⊢ [(¬ R) ⇒ (¬ S)]:∗ |
8 | 7, 5 | wct 44 |
. . . . . 6
⊢ ([(¬ R) ⇒ (¬ S)], S):∗ |
9 | 1 | exmid 186 |
. . . . . 6
⊢
⊤⊧[R ∨ (¬ R)] |
10 | 8, 9 | a1i 28 |
. . . . 5
⊢ ([(¬ R) ⇒ (¬ S)], S)⊧[R
∨ (¬ R)] |
11 | 10 | ax-cb1 29 |
. . . . . 6
⊢ ([(¬ R) ⇒ (¬ S)], S):∗ |
12 | 11, 1 | simpr 23 |
. . . . 5
⊢ (([(¬ R) ⇒ (¬ S)], S),
R)⊧R |
13 | | wfal 125 |
. . . . . . . 8
⊢
⊥:∗ |
14 | 7 | id 25 |
. . . . . . . . . 10
⊢ [(¬ R) ⇒ (¬ S)]⊧[(¬ R) ⇒ (¬ S)] |
15 | 3, 6, 14 | imp 147 |
. . . . . . . . 9
⊢ ([(¬ R) ⇒ (¬ S)], (¬ R))⊧(¬ S) |
16 | 15 | ax-cb1 29 |
. . . . . . . . . 10
⊢ ([(¬ R) ⇒ (¬ S)], (¬ R)):∗ |
17 | 5 | notval 135 |
. . . . . . . . . 10
⊢
⊤⊧[(¬ S) =
[S ⇒ ⊥]] |
18 | 16, 17 | a1i 28 |
. . . . . . . . 9
⊢ ([(¬ R) ⇒ (¬ S)], (¬ R))⊧[(¬ S) = [S ⇒
⊥]] |
19 | 15, 18 | mpbi 72 |
. . . . . . . 8
⊢ ([(¬ R) ⇒ (¬ S)], (¬ R))⊧[S
⇒ ⊥] |
20 | 5, 13, 19 | imp 147 |
. . . . . . 7
⊢ (([(¬ R) ⇒ (¬ S)], (¬ R)),
S)⊧⊥ |
21 | 20 | an32s 55 |
. . . . . 6
⊢ (([(¬ R) ⇒ (¬ S)], S), (¬
R))⊧⊥ |
22 | 1 | pm2.21 143 |
. . . . . 6
⊢
⊥⊧R |
23 | 21, 22 | syl 16 |
. . . . 5
⊢ (([(¬ R) ⇒ (¬ S)], S), (¬
R))⊧R |
24 | 1, 3, 1, 10, 12, 23 | ecase 153 |
. . . 4
⊢ ([(¬ R) ⇒ (¬ S)], S)⊧R |
25 | 24 | ex 148 |
. . 3
⊢ [(¬ R) ⇒ (¬ S)]⊧[S
⇒ R] |
26 | | wtru 40 |
. . 3
⊢
⊤:∗ |
27 | 25, 26 | adantl 51 |
. 2
⊢ (⊤, [(¬
R) ⇒ (¬ S)])⊧[S
⇒ R] |
28 | 27 | ex 148 |
1
⊢
⊤⊧[[(¬ R) ⇒
(¬ S)] ⇒ [S ⇒ R]] |