Proof of Theorem elim2ifim
Step | Hyp | Ref
| Expression |
1 | | exmid 891 |
. . 3
⊢ (𝜑 ∨ ¬ 𝜑) |
2 | | elim2ifim.1 |
. . . . 5
⊢ (𝜑 → 𝜃) |
3 | 2 | ancli 548 |
. . . 4
⊢ (𝜑 → (𝜑 ∧ 𝜃)) |
4 | | pm4.42 1050 |
. . . . . 6
⊢ (¬
𝜑 ↔ ((¬ 𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓))) |
5 | | elim2ifim.2 |
. . . . . . . . . 10
⊢ ((¬
𝜑 ∧ 𝜓) → 𝜏) |
6 | 5 | ex 412 |
. . . . . . . . 9
⊢ (¬
𝜑 → (𝜓 → 𝜏)) |
7 | 6 | ancld 550 |
. . . . . . . 8
⊢ (¬
𝜑 → (𝜓 → (𝜓 ∧ 𝜏))) |
8 | 7 | imp 406 |
. . . . . . 7
⊢ ((¬
𝜑 ∧ 𝜓) → (𝜓 ∧ 𝜏)) |
9 | | elim2ifim.3 |
. . . . . . . . . 10
⊢ ((¬
𝜑 ∧ ¬ 𝜓) → 𝜂) |
10 | 9 | ex 412 |
. . . . . . . . 9
⊢ (¬
𝜑 → (¬ 𝜓 → 𝜂)) |
11 | 10 | ancld 550 |
. . . . . . . 8
⊢ (¬
𝜑 → (¬ 𝜓 → (¬ 𝜓 ∧ 𝜂))) |
12 | 11 | imp 406 |
. . . . . . 7
⊢ ((¬
𝜑 ∧ ¬ 𝜓) → (¬ 𝜓 ∧ 𝜂)) |
13 | 8, 12 | orim12i 905 |
. . . . . 6
⊢ (((¬
𝜑 ∧ 𝜓) ∨ (¬ 𝜑 ∧ ¬ 𝜓)) → ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂))) |
14 | 4, 13 | sylbi 216 |
. . . . 5
⊢ (¬
𝜑 → ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂))) |
15 | 14 | ancli 548 |
. . . 4
⊢ (¬
𝜑 → (¬ 𝜑 ∧ ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂)))) |
16 | 3, 15 | orim12i 905 |
. . 3
⊢ ((𝜑 ∨ ¬ 𝜑) → ((𝜑 ∧ 𝜃) ∨ (¬ 𝜑 ∧ ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂))))) |
17 | 1, 16 | ax-mp 5 |
. 2
⊢ ((𝜑 ∧ 𝜃) ∨ (¬ 𝜑 ∧ ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂)))) |
18 | | elim2if.1 |
. . 3
⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐴 → (𝜒 ↔ 𝜃)) |
19 | | elim2if.2 |
. . 3
⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐵 → (𝜒 ↔ 𝜏)) |
20 | | elim2if.3 |
. . 3
⊢ (if(𝜑, 𝐴, if(𝜓, 𝐵, 𝐶)) = 𝐶 → (𝜒 ↔ 𝜂)) |
21 | 18, 19, 20 | elim2if 30866 |
. 2
⊢ (𝜒 ↔ ((𝜑 ∧ 𝜃) ∨ (¬ 𝜑 ∧ ((𝜓 ∧ 𝜏) ∨ (¬ 𝜓 ∧ 𝜂))))) |
22 | 17, 21 | mpbir 230 |
1
⊢ 𝜒 |