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  12625  fsum00  15971  pcfac  17083  mndifsplit  22957  bposlem2  27618  axcgrid  29500  3o2cs  33108  3o3cs  33109  fprodex01  33463  indsumin  33475  fsum2dsub  35283  finxpreclem2  38407  itg2addnclem  38683  tsan3  39169  xrninxpex  39443  disjimxrn  39875