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  12393  fsum00  15702  pcfac  16808  mndifsplit  22549  bposlem2  27221  axcgrid  28892  3o2cs  32436  3o3cs  32437  fprodex01  32803  indsumin  32838  fsum2dsub  34615  finxpreclem2  37423  itg2addnclem  37710  tsan3  38182  xrninxpex  38425  disjimxrn  38786