Proof of Theorem cases2ALT
Step | Hyp | Ref
| Expression |
1 | | pm3.4 810 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝜑 → 𝜓)) |
2 | | pm2.24 124 |
. . . . 5
⊢ (𝜑 → (¬ 𝜑 → 𝜒)) |
3 | 2 | adantr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (¬ 𝜑 → 𝜒)) |
4 | 1, 3 | jca 516 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |
5 | | pm2.21 123 |
. . . . 5
⊢ (¬
𝜑 → (𝜑 → 𝜓)) |
6 | 5 | adantr 485 |
. . . 4
⊢ ((¬
𝜑 ∧ 𝜒) → (𝜑 → 𝜓)) |
7 | | pm3.4 810 |
. . . 4
⊢ ((¬
𝜑 ∧ 𝜒) → (¬ 𝜑 → 𝜒)) |
8 | 6, 7 | jca 516 |
. . 3
⊢ ((¬
𝜑 ∧ 𝜒) → ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |
9 | 4, 8 | jaoi 855 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) → ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |
10 | | pm2.27 42 |
. . . . . 6
⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓)) |
11 | 10 | imdistani 573 |
. . . . 5
⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → (𝜑 ∧ 𝜓)) |
12 | 11 | orcd 871 |
. . . 4
⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
13 | 12 | adantrr 717 |
. . 3
⊢ ((𝜑 ∧ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) → ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
14 | | pm2.27 42 |
. . . . . 6
⊢ (¬
𝜑 → ((¬ 𝜑 → 𝜒) → 𝜒)) |
15 | 14 | imdistani 573 |
. . . . 5
⊢ ((¬
𝜑 ∧ (¬ 𝜑 → 𝜒)) → (¬ 𝜑 ∧ 𝜒)) |
16 | 15 | olcd 872 |
. . . 4
⊢ ((¬
𝜑 ∧ (¬ 𝜑 → 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
17 | 16 | adantrl 716 |
. . 3
⊢ ((¬
𝜑 ∧ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) → ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
18 | 13, 17 | pm2.61ian 812 |
. 2
⊢ (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
19 | 9, 18 | impbii 212 |
1
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |