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  12510  fsum00  15840  pcfac  16949  mndifsplit  22754  bposlem2  27407  axcgrid  29175  3o2cs  32719  3o3cs  32720  fprodex01  33082  indsumin  33094  fsum2dsub  34911  finxpreclem2  37896  itg2addnclem  38182  tsan3  38654  xrninxpex  38928  disjimxrn  39360