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  4465  ordsuc  4473  reg3exmidlemwe  4488  sotri3  4932  diffisn  6780  onunsnss  6798  fival  6851  suplub2ti  6881  fodjum  7011  addnqprlemfl  7360  addnqprlemfu  7361  mulnqprlemfl  7376  mulnqprlemfu  7377  addcanprleml  7415  addcanprlemu  7416  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  caucvgprlemladdrl  7479  caucvgprprlemaddq  7509  ltletr  7846  apreap  8342  ltleap  8387  uzm1  9349  xrltletr  9583  xaddf  9620  xaddval  9621  iseqf1olemqcl  10252  iseqf1olemnab  10254  iseqf1olemab  10255  exp3val  10288  zfz1isolemiso  10575  ltabs  10852  xrmaxiflemlub  11010  bezoutlemmain  11675  nninfalllem1  13192  nninfall  13193  nninfsellemqall  13200  nninffeq  13205  trilpolemeq1  13222