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  3757  ontriexmidim  4643  preleq  4676  ordsuc  4684  reg3exmidlemwe  4700  sotri3  5160  pw2f1odclem  7086  diffisn  7149  onunsnss  7176  fival  7256  2omap  7268  suplub2ti  7291  fodjum  7436  nninfwlpoimlemginf  7466  3nelsucpw1  7543  3nsssucpw1  7545  addnqprlemfl  7873  addnqprlemfu  7874  mulnqprlemfl  7889  mulnqprlemfu  7890  addcanprleml  7928  addcanprlemu  7929  cauappcvgprlemladdru  7970  cauappcvgprlemladdrl  7971  caucvgprlemladdrl  7992  caucvgprprlemaddq  8022  ltletr  8362  apreap  8860  ltleap  8905  uzm1  9884  xrltletr  10139  xaddf  10176  xaddval  10177  iseqf1olemqcl  10860  iseqf1olemnab  10862  iseqf1olemab  10863  exp3val  10902  zfz1isolemiso  11207  ltabs  11768  xrmaxiflemlub  11929  fprodsplitdc  12278  fprodcl2lem  12287  bitsfzo  12637  bezoutlemmain  12690  nninfctlemfo  12732  4sqlem17  13101  4sqlem18  13102  plycoeid3  15614  dvply1  15622  perfectlem2  15860  lgsval  15869  lgsfvalg  15870  lgsdilem  15892  lgsdir  15900  lgsabs1  15904  gausslemma2dlem1f1o  15925  lgseisenlem1  15935  2sqlem7  15986  clwwlknnn  16399  nninfalllem1  16778  nninfall  16779  nninfsellemqall  16785  nninffeq  16790  nninfnfiinf  16793  trilpolemeq1  16816  nconstwlpolem  16842