Metamath Proof Explorer

Theorem olcs

Description: Deduction eliminating disjunct. (Contributed by NM, 21-Jun-1994) (Proof shortened by Wolf Lammen, 3-Oct-2013)

Ref Expression
Hypothesis olcs.1 
|- ( ( ph \/ ps ) -> ch )
Assertion olcs 
|- ( ps -> ch )

Proof

Step Hyp Ref Expression
1 olcs.1 
 |-  ( ( ph \/ ps ) -> ch )
2 1 orcoms 
 |-  ( ( ps \/ ph ) -> ch )
3 2 orcs 
 |-  ( ps -> ch )