Theorem olcs 877

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  0nn0  12452  fsum00  15761  pcfac  16870  mndifsplit  22601  bposlem2  27248  axcgrid  28985  3o2cs  32531  3o3cs  32532  fprodex01  32898  indsumin  32921  fsum2dsub  34751  finxpreclem2  37706  itg2addnclem  37992  tsan3  38464  xrninxpex  38738  disjimxrn  39170