Theorem ecased 1386

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

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

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 620  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1387  ecase2d  1388  rabsnif  3763  ontriexmidim  4649  preleq  4682  ordsuc  4690  reg3exmidlemwe  4706  sotri3  5166  pw2f1odclem  7100  diffisn  7163  onunsnss  7190  fival  7270  2omap  7282  suplub2ti  7305  fodjum  7450  nninfwlpoimlemginf  7480  3nelsucpw1  7557  3nsssucpw1  7559  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemfl  7906  mulnqprlemfu  7907  addcanprleml  7945  addcanprlemu  7946  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  caucvgprprlemaddq  8039  ltletr  8379  apreap  8879  ltleap  8924  uzm1  9906  xrltletr  10162  xaddf  10199  xaddval  10200  iseqf1olemqcl  10888  iseqf1olemnab  10890  iseqf1olemab  10891  exp3val  10930  zfz1isolemiso  11239  ltabs  11801  xrmaxiflemlub  11962  fprodsplitdc  12311  fprodcl2lem  12320  bitsfzo  12670  bezoutlemmain  12723  nninfctlemfo  12765  4sqlem17  13134  4sqlem18  13135  plycoeid3  15752  dvply1  15760  perfectlem2  15998  lgsval  16007  lgsfvalg  16008  lgsdilem  16030  lgsdir  16038  lgsabs1  16042  gausslemma2dlem1f1o  16063  lgseisenlem1  16073  2sqlem7  16124  clwwlknnn  16537  nninfalllem1  16926  nninfall  16927  nninfsellemqall  16933  nninffeq  16938  nninfnfiinf  16941  trilpolemeq1  16964  nconstwlpolem  16990