Theorem ecased 1292

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 301	. 2 ⊢ (𝜑 → (¬ 𝜒 ∧ (𝜓 ∨ 𝜒)))
4		orel2 683	. . 3 ⊢ (¬ 𝜒 → ((𝜓 ∨ 𝜒) → 𝜓))
5	4	imp 123	. 2 ⊢ ((¬ 𝜒 ∧ (𝜓 ∨ 𝜒)) → 𝜓)
6	3, 5	syl 14	1 ⊢ (𝜑 → 𝜓)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∨ wo 667

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 583  ax-io 668

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ecase23d  1293  preleq  4399  ordsuc  4407  reg3exmidlemwe  4422  sotri3  4863  diffisn  6689  onunsnss  6707  suplub2ti  6776  fodjum  6889  addnqprlemfl  7215  addnqprlemfu  7216  mulnqprlemfl  7231  mulnqprlemfu  7232  addcanprleml  7270  addcanprlemu  7271  cauappcvgprlemladdru  7312  cauappcvgprlemladdrl  7313  caucvgprlemladdrl  7334  caucvgprprlemaddq  7364  ltletr  7671  apreap  8161  ltleap  8204  uzm1  9148  xrltletr  9373  xaddf  9410  xaddval  9411  iseqf1olemqcl  10036  iseqf1olemnab  10038  iseqf1olemab  10039  exp3val  10072  zfz1isolemiso  10359  ltabs  10635  xrmaxiflemlub  10791  bezoutlemmain  11414  nninfalllem1  12604  nninfall  12605  nninfsellemqall  12612