![]() |
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 644 | . . 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 628 |
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 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: ecase23d 1239 preleq 4233 ordsuc 4241 sotri3 4666 addnqprlemfl 6540 addnqprlemfu 6541 addcanprleml 6588 addcanprlemu 6589 cauappcvgprlemladdru 6628 cauappcvgprlemladdrl 6629 caucvgprlemladdrl 6649 ltletr 6904 apreap 7371 ltleap 7413 uzm1 8279 xrltletr 8493 |
Copyright terms: Public domain | W3C validator |