![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ecased | GIF version |
Description: Deduction form of disjunctive syllogism. (Contributed by Jim Kingdon, 9-Dec-2017.) |
Ref | Expression |
---|---|
ecased.1 | ⊢ (𝜑 → ¬ 𝜒) |
ecased.2 | ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
Ref | Expression |
---|---|
ecased | ⊢ (𝜑 → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ecased.1 | . . 3 ⊢ (𝜑 → ¬ 𝜒) | |
2 | ecased.2 | . . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜒)) | |
3 | 1, 2 | jca 290 | . 2 ⊢ (𝜑 → (¬ 𝜒 ∧ (𝜓 ∨ 𝜒))) |
4 | orel2 645 | . . 3 ⊢ (¬ 𝜒 → ((𝜓 ∨ 𝜒) → 𝜓)) | |
5 | 4 | imp 115 | . 2 ⊢ ((¬ 𝜒 ∧ (𝜓 ∨ 𝜒)) → 𝜓) |
6 | 3, 5 | syl 14 | 1 ⊢ (𝜑 → 𝜓) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∧ wa 97 ∨ wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in2 545 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ecase23d 1240 preleq 4279 ordsuc 4287 reg3exmidlemwe 4303 sotri3 4723 diffisn 6350 onunsnss 6355 addnqprlemfl 6657 addnqprlemfu 6658 mulnqprlemfl 6673 mulnqprlemfu 6674 addcanprleml 6712 addcanprlemu 6713 cauappcvgprlemladdru 6754 cauappcvgprlemladdrl 6755 caucvgprlemladdrl 6776 caucvgprprlemaddq 6806 ltletr 7107 apreap 7578 ltleap 7621 uzm1 8503 xrltletr 8723 ltabs 9683 |
Copyright terms: Public domain | W3C validator |