Theorem ecased 1327

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ecase23d  1328  preleq  4470  ordsuc  4478  reg3exmidlemwe  4493  sotri3  4937  diffisn  6787  onunsnss  6805  fival  6858  suplub2ti  6888  fodjum  7018  addnqprlemfl  7367  addnqprlemfu  7368  mulnqprlemfl  7383  mulnqprlemfu  7384  addcanprleml  7422  addcanprlemu  7423  cauappcvgprlemladdru  7464  cauappcvgprlemladdrl  7465  caucvgprlemladdrl  7486  caucvgprprlemaddq  7516  ltletr  7853  apreap  8349  ltleap  8394  uzm1  9356  xrltletr  9590  xaddf  9627  xaddval  9628  iseqf1olemqcl  10259  iseqf1olemnab  10261  iseqf1olemab  10262  exp3val  10295  zfz1isolemiso  10582  ltabs  10859  xrmaxiflemlub  11017  bezoutlemmain  11686  nninfalllem1  13203  nninfall  13204  nninfsellemqall  13211  nninffeq  13216  trilpolemeq1  13233