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  3742  ontriexmidim  4626  preleq  4659  ordsuc  4667  reg3exmidlemwe  4683  sotri3  5142  pw2f1odclem  7063  diffisn  7125  onunsnss  7152  fival  7212  suplub2ti  7243  fodjum  7388  nninfwlpoimlemginf  7418  3nelsucpw1  7495  3nsssucpw1  7497  addnqprlemfl  7822  addnqprlemfu  7823  mulnqprlemfl  7838  mulnqprlemfu  7839  addcanprleml  7877  addcanprlemu  7878  cauappcvgprlemladdru  7919  cauappcvgprlemladdrl  7920  caucvgprlemladdrl  7941  caucvgprprlemaddq  7971  ltletr  8312  apreap  8810  ltleap  8855  uzm1  9830  xrltletr  10085  xaddf  10122  xaddval  10123  iseqf1olemqcl  10805  iseqf1olemnab  10807  iseqf1olemab  10808  exp3val  10847  zfz1isolemiso  11147  ltabs  11708  xrmaxiflemlub  11869  fprodsplitdc  12218  fprodcl2lem  12227  bitsfzo  12577  bezoutlemmain  12630  nninfctlemfo  12672  4sqlem17  13041  4sqlem18  13042  plycoeid3  15548  dvply1  15556  perfectlem2  15794  lgsval  15803  lgsfvalg  15804  lgsdilem  15826  lgsdir  15834  lgsabs1  15838  gausslemma2dlem1f1o  15859  lgseisenlem1  15869  2sqlem7  15920  clwwlknnn  16333  2omap  16695  nninfalllem1  16714  nninfall  16715  nninfsellemqall  16721  nninffeq  16726  nninfnfiinf  16729  trilpolemeq1  16752  nconstwlpolem  16778