Step | Hyp | Ref
| Expression |
1 | | pm2.521g 174 |
. . . . . 6
⊢ (¬
(𝜑 → 𝜓) → (𝜓 → 𝜒)) |
2 | 1 | a1d 25 |
. . . . 5
⊢ (¬
(𝜑 → 𝜓) → (𝜑 → (𝜓 → 𝜒))) |
3 | | ax-1 6 |
. . . . . 6
⊢ (𝜒 → (𝜓 → 𝜒)) |
4 | 3 | a1d 25 |
. . . . 5
⊢ (𝜒 → (𝜑 → (𝜓 → 𝜒))) |
5 | 2, 4 | ja 186 |
. . . 4
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜑 → (𝜓 → 𝜒))) |
6 | | ax-2 7 |
. . . . 5
⊢ ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → (𝜑 → 𝜒))) |
7 | 6 | com3r 87 |
. . . 4
⊢ (𝜑 → ((𝜑 → (𝜓 → 𝜒)) → ((𝜑 → 𝜓) → 𝜒))) |
8 | 5, 7 | impbid2 225 |
. . 3
⊢ (𝜑 → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) |
9 | | ax-1 6 |
. . . 4
⊢ (𝜒 → ((𝜑 → 𝜓) → 𝜒)) |
10 | 9, 4 | 2thd 265 |
. . 3
⊢ (𝜒 → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) |
11 | 8, 10 | jaoi 856 |
. 2
⊢ ((𝜑 ∨ 𝜒) → (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) |
12 | | jarl 125 |
. . . . 5
⊢ (((𝜑 → 𝜓) → 𝜒) → (¬ 𝜑 → 𝜒)) |
13 | 12 | orrd 862 |
. . . 4
⊢ (((𝜑 → 𝜓) → 𝜒) → (𝜑 ∨ 𝜒)) |
14 | 13 | a1d 25 |
. . 3
⊢ (((𝜑 → 𝜓) → 𝜒) → ((𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒))) |
15 | | simplim 167 |
. . . . 5
⊢ (¬
(𝜑 → (𝜓 → 𝜒)) → 𝜑) |
16 | 15 | orcd 872 |
. . . 4
⊢ (¬
(𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒)) |
17 | 16 | a1i 11 |
. . 3
⊢ (¬
((𝜑 → 𝜓) → 𝜒) → (¬ (𝜑 → (𝜓 → 𝜒)) → (𝜑 ∨ 𝜒))) |
18 | 14, 17 | bija 382 |
. 2
⊢ ((((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒))) → (𝜑 ∨ 𝜒)) |
19 | 11, 18 | impbii 208 |
1
⊢ ((𝜑 ∨ 𝜒) ↔ (((𝜑 → 𝜓) → 𝜒) ↔ (𝜑 → (𝜓 → 𝜒)))) |