Theorem olcs 890

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

This proof depends on syntax axioms:   → wi 4   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  0nn0  12661  fsum00  16009  pcfac  17121  mndifsplit  23006  bposlem2  27669  axcgrid  29551  3o2cs  33159  3o3cs  33160  fprodex01  33512  indsumin  33524  fsum2dsub  35347  finxpreclem2  38581  itg2addnclem  38857  tsan3  39341  xrninxpex  39615  disjimxrn  40047