Theorem olcs 887

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

Syntax hints:   → wi 4   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  0nn0  12493  fsum00  15809  pcfac  16918  mndifsplit  22676  bposlem2  27326  axcgrid  29063  3o2cs  32609  3o3cs  32610  fprodex01  32977  indsumin  33000  fsum2dsub  34865  finxpreclem2  37848  itg2addnclem  38134  tsan3  38606  xrninxpex  38880  disjimxrn  39312