|   | 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 872 | . 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜒) | 
| 3 | 2 | orcs 875 | 1 ⊢ (𝜓 → 𝜒) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∨ wo 847 | 
| 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 207 df-or 848 | 
| This theorem is referenced by: 0nn0 12543 fsum00 15835 pcfac 16938 mndifsplit 22643 bposlem2 27330 axcgrid 28932 3o2cs 32482 3o3cs 32483 fprodex01 32828 indsumin 32848 fsum2dsub 34623 finxpreclem2 37392 itg2addnclem 37679 tsan3 38151 ecexALTV 38333 cnvepimaex 38338 xrninxpex 38396 disjimxrn 38751 | 
| Copyright terms: Public domain | W3C validator |