Theorem olcs 882

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 878	. 2 ⊢ ((𝜓 ∨ 𝜑) → 𝜒)
3	2	orcs 881	1 ⊢ (𝜓 → 𝜒)

Syntax hints:   → wi 4   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  0nn0  12450  fsum00  15759  pcfac  16868  mndifsplit  22626  bposlem2  27273  axcgrid  29010  3o2cs  32556  3o3cs  32557  fprodex01  32924  indsumin  32947  fsum2dsub  34798  finxpreclem2  37759  itg2addnclem  38045  tsan3  38517  xrninxpex  38791  disjimxrn  39223