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  12457  fsum00  15764  pcfac  16870  mndifsplit  22523  bposlem2  27196  axcgrid  28843  3o2cs  32391  3o3cs  32392  fprodex01  32750  indsumin  32785  fsum2dsub  34598  finxpreclem2  37378  itg2addnclem  37665  tsan3  38137  xrninxpex  38380  disjimxrn  38741