Theorem ecased 1280

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 102   ∨ wo 661

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 577  ax-io 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  ecase23d  1281  preleq  4298  ordsuc  4306  reg3exmidlemwe  4321  sotri3  4743  diffisn  6377  onunsnss  6383  suplub2ti  6414  addnqprlemfl  6749  addnqprlemfu  6750  mulnqprlemfl  6765  mulnqprlemfu  6766  addcanprleml  6804  addcanprlemu  6805  cauappcvgprlemladdru  6846  cauappcvgprlemladdrl  6847  caucvgprlemladdrl  6868  caucvgprprlemaddq  6898  ltletr  7200  apreap  7687  ltleap  7730  uzm1  8649  xrltletr  8877  ltabs  9973  bezoutlemmain  10387