Proof of Theorem rp-fakeimass
Step | Hyp | Ref
| Expression |
1 | | ax-1 6 |
. . . . . . . 8
⊢ (𝜓 → (𝜑 → 𝜓)) |
2 | 1 | con3i 152 |
. . . . . . 7
⊢ (¬
(𝜑 → 𝜓) → ¬ 𝜓) |
3 | 2 | pm2.21d 119 |
. . . . . 6
⊢ (¬
(𝜑 → 𝜓) → (𝜓 → 𝜒)) |
4 | 3 | a1d 25 |
. . . . 5
⊢ (¬
(𝜑 → 𝜓) → (𝜑 → (𝜓 → 𝜒))) |
5 | | ax-1 6 |
. . . . . 6
⊢ (𝜒 → (𝜓 → 𝜒)) |
6 | 5 | a1d 25 |
. . . . 5
⊢ (𝜒 → (𝜑 → (𝜓 → 𝜒))) |
7 | 4, 6 | ja 175 |
. . . 4
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) |
8 | | ax-2 7 |
. . . . 5
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) |
9 | 8 | com3r 87 |
. . . 4
⊢ (𝜑 → ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))) |
10 | 7, 9 | impbid2 218 |
. . 3
⊢ (𝜑 → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) |
11 | | ax-1 6 |
. . . 4
⊢ (𝜒 → ((𝜑 → 𝜓) → 𝜒)) |
12 | 11, 6 | 2thd 257 |
. . 3
⊢ (𝜒 → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) |
13 | 10, 12 | jaoi 846 |
. 2
⊢ ((𝜑 ∨ 𝜒) → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) |
14 | | jarl 123 |
. . . . 5
⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒)) |
15 | 14 | orrd 852 |
. . . 4
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜑 ∨ 𝜒)) |
16 | 15 | a1d 25 |
. . 3
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒))) |
17 | | simplim 165 |
. . . . 5
⊢ (¬
(𝜑 → (𝜓 → 𝜒)) → 𝜑) |
18 | 17 | orcd 862 |
. . . 4
⊢ (¬
(𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒)) |
19 | 18 | a1i 11 |
. . 3
⊢ (¬
((𝜑 → 𝜓) → 𝜒) → (¬ (𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒))) |
20 | 16, 19 | bija 372 |
. 2
⊢ ((((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) → (𝜑 ∨ 𝜒)) |
21 | 13, 20 | impbii 201 |
1
⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) |