Theorem ecased 1383

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

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

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 618  ax-io 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1384  ecase2d  1385  ontriexmidim  4611  preleq  4644  ordsuc  4652  reg3exmidlemwe  4668  sotri3  5123  pw2f1odclem  6983  diffisn  7043  onunsnss  7067  fival  7125  suplub2ti  7156  fodjum  7301  nninfwlpoimlemginf  7331  3nelsucpw1  7407  3nsssucpw1  7409  addnqprlemfl  7734  addnqprlemfu  7735  mulnqprlemfl  7750  mulnqprlemfu  7751  addcanprleml  7789  addcanprlemu  7790  cauappcvgprlemladdru  7831  cauappcvgprlemladdrl  7832  caucvgprlemladdrl  7853  caucvgprprlemaddq  7883  ltletr  8224  apreap  8722  ltleap  8767  uzm1  9741  xrltletr  9991  xaddf  10028  xaddval  10029  iseqf1olemqcl  10708  iseqf1olemnab  10710  iseqf1olemab  10711  exp3val  10750  zfz1isolemiso  11048  ltabs  11584  xrmaxiflemlub  11745  fprodsplitdc  12093  fprodcl2lem  12102  bitsfzo  12452  bezoutlemmain  12505  nninfctlemfo  12547  4sqlem17  12916  4sqlem18  12917  plycoeid3  15416  dvply1  15424  perfectlem2  15659  lgsval  15668  lgsfvalg  15669  lgsdilem  15691  lgsdir  15699  lgsabs1  15703  gausslemma2dlem1f1o  15724  lgseisenlem1  15734  2sqlem7  15785  2omap  16290  nninfalllem1  16305  nninfall  16306  nninfsellemqall  16312  nninffeq  16317  nninfnfiinf  16320  trilpolemeq1  16339  nconstwlpolem  16364