Theorem ecased 1385

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1386  ecase2d  1387  rabsnif  3738  ontriexmidim  4620  preleq  4653  ordsuc  4661  reg3exmidlemwe  4677  sotri3  5135  pw2f1odclem  7020  diffisn  7082  onunsnss  7109  fival  7169  suplub2ti  7200  fodjum  7345  nninfwlpoimlemginf  7375  3nelsucpw1  7452  3nsssucpw1  7454  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemfl  7795  mulnqprlemfu  7796  addcanprleml  7834  addcanprlemu  7835  cauappcvgprlemladdru  7876  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  caucvgprprlemaddq  7928  ltletr  8269  apreap  8767  ltleap  8812  uzm1  9787  xrltletr  10042  xaddf  10079  xaddval  10080  iseqf1olemqcl  10762  iseqf1olemnab  10764  iseqf1olemab  10765  exp3val  10804  zfz1isolemiso  11104  ltabs  11652  xrmaxiflemlub  11813  fprodsplitdc  12162  fprodcl2lem  12171  bitsfzo  12521  bezoutlemmain  12574  nninfctlemfo  12616  4sqlem17  12985  4sqlem18  12986  plycoeid3  15487  dvply1  15495  perfectlem2  15730  lgsval  15739  lgsfvalg  15740  lgsdilem  15762  lgsdir  15770  lgsabs1  15774  gausslemma2dlem1f1o  15795  lgseisenlem1  15805  2sqlem7  15856  clwwlknnn  16269  2omap  16620  nninfalllem1  16636  nninfall  16637  nninfsellemqall  16643  nninffeq  16648  nninfnfiinf  16651  trilpolemeq1  16670  nconstwlpolem  16695