![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > olcs | Structured version Visualization version GIF version |
Description: Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994.) (Proof shortened by Wolf Lammen, 3-Oct-2013.) |
Ref | Expression |
---|---|
olcs.1 | ⊢ ((𝜑 ∨ 𝜓) → 𝜒) |
Ref | Expression |
---|---|
olcs | ⊢ (𝜓 → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | olcs.1 | . . 3 ⊢ ((𝜑 ∨ 𝜓) → 𝜒) | |
2 | 1 | orcoms 871 | . 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜒) |
3 | 2 | orcs 874 | 1 ⊢ (𝜓 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 |
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 206 df-or 847 |
This theorem is referenced by: 0nn0 12483 fsum00 15740 pcfac 16828 mndifsplit 22120 bposlem2 26768 axcgrid 28154 3o2cs 31682 3o3cs 31683 fprodex01 32009 indsumin 32958 fsum2dsub 33557 finxpreclem2 36209 itg2addnclem 36477 tsan3 36949 ecexALTV 37138 cnvepimaex 37143 xrninxpex 37202 disjimxrn 37557 |
Copyright terms: Public domain | W3C validator |