Theorem olcs 875

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

Syntax hints:   → wi 4   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  0nn0  12483  fsum00  15740  pcfac  16828  mndifsplit  22120  bposlem2  26768  axcgrid  28154  3o2cs  31682  3o3cs  31683  fprodex01  32009  indsumin  32958  fsum2dsub  33557  finxpreclem2  36209  itg2addnclem  36477  tsan3  36949  ecexALTV  37138  cnvepimaex  37143  xrninxpex  37202  disjimxrn  37557