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 869 | . 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜒) |
3 | 2 | orcs 872 | 1 ⊢ (𝜓 → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 844 |
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 845 |
This theorem is referenced by: 0nn0 12349 fsum00 15609 pcfac 16697 mndifsplit 21891 bposlem2 26539 axcgrid 27573 3o2cs 31101 3o3cs 31102 fprodex01 31426 indsumin 32288 fsum2dsub 32887 finxpreclem2 35674 itg2addnclem 35941 tsan3 36414 ecexALTV 36605 cnvepimaex 36610 xrninxpex 36669 disjimxrn 37024 |
Copyright terms: Public domain | W3C validator |