Theorem ecased 1239

Description: Deduction form of disjunctive syllogism. (Contributed by Jim Kingdon, 9-Dec-2017.)

Hypotheses

Ref	Expression
ecased.1	⊢ (𝜑 → ¬ 𝜒)
ecased.2	⊢ (𝜑 → (𝜓 ∨ 𝜒))

Assertion

Ref	Expression
ecased	⊢ (𝜑 → 𝜓)

Proof of Theorem ecased

Step	Hyp	Ref	Expression
1		ecased.1	. . 3 ⊢ (𝜑 → ¬ 𝜒)
2		ecased.2	. . 3 ⊢ (𝜑 → (𝜓 ∨ 𝜒))
3	1, 2	jca 290	. 2 ⊢ (𝜑 → (¬ 𝜒 ∧ (𝜓 ∨ 𝜒)))
4		orel2 645	. . 3 ⊢ (¬ 𝜒 → ((𝜓 ∨ 𝜒) → 𝜓))
5	4	imp 115	. 2 ⊢ ((¬ 𝜒 ∧ (𝜓 ∨ 𝜒)) → 𝜓)
6	3, 5	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in2 545  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ecase23d  1240  preleq  4279  ordsuc  4287  reg3exmidlemwe  4303  sotri3  4723  diffisn  6350  onunsnss  6355  addnqprlemfl  6657  addnqprlemfu  6658  mulnqprlemfl  6673  mulnqprlemfu  6674  addcanprleml  6712  addcanprlemu  6713  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemladdrl  6776  caucvgprprlemaddq  6806  ltletr  7107  apreap  7578  ltleap  7621  uzm1  8503  xrltletr  8723  ltabs  9683