Theorem olcs 889

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

Hypothesis

Ref	Expression
olcs.1	⊢ ((𝜑 ∨ 𝜓) → 𝜒)

Assertion

Ref	Expression
olcs	⊢ (𝜓 → 𝜒)

Proof of Theorem olcs

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

Syntax hints:   → wi 4   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  0nn0  12520  fsum00  15852  pcfac  16960  mndifsplit  22774  bposlem2  27427  axcgrid  29244  3o2cs  32788  3o3cs  32789  fprodex01  33147  indsumin  33159  fsum2dsub  34972  finxpreclem2  38014  itg2addnclem  38300  tsan3  38770  xrninxpex  39044  disjimxrn  39476