![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ecase23d | GIF version |
Description: Variation of ecased 1349 with three disjuncts instead of two. (Contributed by NM, 22-Apr-1994.) (Revised by Jim Kingdon, 9-Dec-2017.) |
Ref | Expression |
---|---|
ecase23d.1 | ⊢ (𝜑 → ¬ 𝜒) |
ecase23d.2 | ⊢ (𝜑 → ¬ 𝜃) |
ecase23d.3 | ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) |
Ref | Expression |
---|---|
ecase23d | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ecase23d.1 | . 2 ⊢ (𝜑 → ¬ 𝜒) | |
2 | ecase23d.2 | . . 3 ⊢ (𝜑 → ¬ 𝜃) | |
3 | ecase23d.3 | . . . 4 ⊢ (𝜑 → (𝜓 ∨ 𝜒 ∨ 𝜃)) | |
4 | df-3or 979 | . . . 4 ⊢ ((𝜓 ∨ 𝜒 ∨ 𝜃) ↔ ((𝜓 ∨ 𝜒) ∨ 𝜃)) | |
5 | 3, 4 | sylib 122 | . . 3 ⊢ (𝜑 → ((𝜓 ∨ 𝜒) ∨ 𝜃)) |
6 | 2, 5 | ecased 1349 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
7 | 1, 6 | ecased 1349 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 708 ∨ w3o 977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in2 615 ax-io 709 |
This theorem depends on definitions: df-bi 117 df-3or 979 |
This theorem is referenced by: iseqf1olemklt 10485 xrmaxiflemcl 11253 xrmaxifle 11254 xrmaxiflemab 11255 xrmaxiflemlub 11256 ennnfonelemex 12415 mulgval 12986 mulgfng 12987 subgmulg 13048 |
Copyright terms: Public domain | W3C validator |