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	⊢ ( ( 𝜑 ∨ 𝜓 ) → 𝜒 )
Assertion	olcs	⊢ ( 𝜓 → 𝜒 )

Proof

Step	Hyp	Ref	Expression
1		olcs.1	⊢ ( ( 𝜑 ∨ 𝜓 ) → 𝜒 )
2	1	orcoms	⊢ ( ( 𝜓 ∨ 𝜑 ) → 𝜒 )
3	2	orcs	⊢ ( 𝜓 → 𝜒 )