Mathbox for Jeff Hankins |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > ecase13d | Structured version Visualization version GIF version |
Description: Deduction for elimination by cases. (Contributed by Jeff Hankins, 18-Aug-2009.) |
Ref | Expression |
---|---|
ecase13d.1 | ⊢ (𝜑 → ¬ 𝜒) |
ecase13d.2 | ⊢ (𝜑 → ¬ 𝜃) |
ecase13d.3 | ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) |
Ref | Expression |
---|---|
ecase13d | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ecase13d.2 | . 2 ⊢ (𝜑 → ¬ 𝜃) | |
2 | ecase13d.1 | . . . 4 ⊢ (𝜑 → ¬ 𝜒) | |
3 | ecase13d.3 | . . . . 5 ⊢ (𝜑 → (𝜒 ∨ 𝜓 ∨ 𝜃)) | |
4 | 3orass 1092 | . . . . . 6 ⊢ ((𝜒 ∨ 𝜓 ∨ 𝜃) ↔ (𝜒 ∨ (𝜓 ∨ 𝜃))) | |
5 | df-or 848 | . . . . . 6 ⊢ ((𝜒 ∨ (𝜓 ∨ 𝜃)) ↔ (¬ 𝜒 → (𝜓 ∨ 𝜃))) | |
6 | 4, 5 | bitri 278 | . . . . 5 ⊢ ((𝜒 ∨ 𝜓 ∨ 𝜃) ↔ (¬ 𝜒 → (𝜓 ∨ 𝜃))) |
7 | 3, 6 | sylib 221 | . . . 4 ⊢ (𝜑 → (¬ 𝜒 → (𝜓 ∨ 𝜃))) |
8 | 2, 7 | mpd 15 | . . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜃)) |
9 | orcom 870 | . . . 4 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓)) | |
10 | df-or 848 | . . . 4 ⊢ ((𝜃 ∨ 𝜓) ↔ (¬ 𝜃 → 𝜓)) | |
11 | 9, 10 | bitri 278 | . . 3 ⊢ ((𝜓 ∨ 𝜃) ↔ (¬ 𝜃 → 𝜓)) |
12 | 8, 11 | sylib 221 | . 2 ⊢ (𝜑 → (¬ 𝜃 → 𝜓)) |
13 | 1, 12 | mpd 15 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 847 ∨ w3o 1088 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 210 df-or 848 df-3or 1090 |
This theorem is referenced by: ivthALT 34261 |
Copyright terms: Public domain | W3C validator |