Proof of Theorem cases2ALT
Step | Hyp | Ref
| Expression |
1 | | pm3.4 807 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝜑 → 𝜓)) |
2 | | pm2.24 124 |
. . . . 5
⊢ (𝜑 → (¬ 𝜑 → 𝜒)) |
3 | 2 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (¬ 𝜑 → 𝜒)) |
4 | 1, 3 | jca 512 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |
5 | | pm2.21 123 |
. . . . 5
⊢ (¬
𝜑 → (𝜑 → 𝜓)) |
6 | 5 | adantr 481 |
. . . 4
⊢ ((¬
𝜑 ∧ 𝜒) → (𝜑 → 𝜓)) |
7 | | pm3.4 807 |
. . . 4
⊢ ((¬
𝜑 ∧ 𝜒) → (¬ 𝜑 → 𝜒)) |
8 | 6, 7 | jca 512 |
. . 3
⊢ ((¬
𝜑 ∧ 𝜒) → ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |
9 | 4, 8 | jaoi 854 |
. 2
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) → ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |
10 | | pm2.27 42 |
. . . . . 6
⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓)) |
11 | 10 | imdistani 569 |
. . . . 5
⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → (𝜑 ∧ 𝜓)) |
12 | 11 | orcd 870 |
. . . 4
⊢ ((𝜑 ∧ (𝜑 → 𝜓)) → ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
13 | 12 | adantrr 714 |
. . 3
⊢ ((𝜑 ∧ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) → ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
14 | | pm2.27 42 |
. . . . . 6
⊢ (¬
𝜑 → ((¬ 𝜑 → 𝜒) → 𝜒)) |
15 | 14 | imdistani 569 |
. . . . 5
⊢ ((¬
𝜑 ∧ (¬ 𝜑 → 𝜒)) → (¬ 𝜑 ∧ 𝜒)) |
16 | 15 | olcd 871 |
. . . 4
⊢ ((¬
𝜑 ∧ (¬ 𝜑 → 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
17 | 16 | adantrl 713 |
. . 3
⊢ ((¬
𝜑 ∧ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) → ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
18 | 13, 17 | pm2.61ian 809 |
. 2
⊢ (((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒)) → ((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒))) |
19 | 9, 18 | impbii 208 |
1
⊢ (((𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ 𝜒)) ↔ ((𝜑 → 𝜓) ∧ (¬ 𝜑 → 𝜒))) |