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  12443  fsum00  15752  pcfac  16861  mndifsplit  22611  bposlem2  27262  axcgrid  28999  3o2cs  32546  3o3cs  32547  fprodex01  32913  indsumin  32936  fsum2dsub  34767  finxpreclem2  37720  itg2addnclem  38006  tsan3  38478  xrninxpex  38752  disjimxrn  39184