Theorem ecased 1328

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

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

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 605  ax-io 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ecase23d  1329  preleq  4478  ordsuc  4486  reg3exmidlemwe  4501  sotri3  4945  diffisn  6795  onunsnss  6813  fival  6866  suplub2ti  6896  fodjum  7026  addnqprlemfl  7391  addnqprlemfu  7392  mulnqprlemfl  7407  mulnqprlemfu  7408  addcanprleml  7446  addcanprlemu  7447  cauappcvgprlemladdru  7488  cauappcvgprlemladdrl  7489  caucvgprlemladdrl  7510  caucvgprprlemaddq  7540  ltletr  7877  apreap  8373  ltleap  8418  uzm1  9380  xrltletr  9620  xaddf  9657  xaddval  9658  iseqf1olemqcl  10290  iseqf1olemnab  10292  iseqf1olemab  10293  exp3val  10326  zfz1isolemiso  10614  ltabs  10891  xrmaxiflemlub  11049  bezoutlemmain  11722  nninfalllem1  13378  nninfall  13379  nninfsellemqall  13386  nninffeq  13391  trilpolemeq1  13408