Theorem olcs 876

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

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  0nn0  12543  fsum00  15835  pcfac  16938  mndifsplit  22643  bposlem2  27330  axcgrid  28932  3o2cs  32482  3o3cs  32483  fprodex01  32828  indsumin  32848  fsum2dsub  34623  finxpreclem2  37392  itg2addnclem  37679  tsan3  38151  ecexALTV  38333  cnvepimaex  38338  xrninxpex  38396  disjimxrn  38751