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  12428  fsum00  15733  pcfac  16839  mndifsplit  22592  bposlem2  27264  axcgrid  29001  3o2cs  32547  3o3cs  32548  fprodex01  32916  indsumin  32953  fsum2dsub  34784  finxpreclem2  37639  itg2addnclem  37916  tsan3  38388  xrninxpex  38662  disjimxrn  39094