Theorem ecased 1390

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

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 720

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1391  ecase2d  1392  rabsnif  3777  ontriexmidim  4667  preleq  4700  ordsuc  4708  reg3exmidlemwe  4724  sotri3  5184  pw2f1odclem  7128  diffisn  7191  onunsnss  7218  fival  7298  2omap  7312  suplub2ti  7335  fodjum  7480  nninfwlpoimlemginf  7510  3nelsucpw1  7587  3nsssucpw1  7589  addnqprlemfl  7920  addnqprlemfu  7921  mulnqprlemfl  7936  mulnqprlemfu  7937  addcanprleml  7975  addcanprlemu  7976  cauappcvgprlemladdru  8017  cauappcvgprlemladdrl  8018  caucvgprlemladdrl  8039  caucvgprprlemaddq  8069  ltletr  8409  apreap  8909  ltleap  8954  uzm1  9936  xrltletr  10192  xaddf  10229  xaddval  10230  iseqf1olemqcl  10919  iseqf1olemnab  10921  iseqf1olemab  10922  exp3val  10961  zfz1isolemiso  11274  ltabs  11836  xrmaxiflemlub  11997  fprodsplitdc  12346  fprodcl2lem  12355  bitsfzo  12705  bezoutlemmain  12758  nninfctlemfo  12800  4sqlem17  13169  4sqlem18  13170  plycoeid3  15841  dvply1  15849  perfectlem2  16097  lgsval  16106  lgsfvalg  16107  lgsdilem  16129  lgsdir  16137  lgsabs1  16141  gausslemma2dlem1f1o  16162  lgseisenlem1  16172  2sqlem7  16223  clwwlknnn  16636  nninfalllem1  17025  nninfall  17026  nninfsellemqall  17032  nninffeq  17037  nninfnfiinf  17040  trilpolemeq1  17063  nconstwlpolem  17089