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  rabsnif  3736  ontriexmidim  4618  preleq  4651  ordsuc  4659  reg3exmidlemwe  4675  sotri3  5133  pw2f1odclem  7015  diffisn  7077  onunsnss  7104  fival  7163  suplub2ti  7194  fodjum  7339  nninfwlpoimlemginf  7369  3nelsucpw1  7445  3nsssucpw1  7447  addnqprlemfl  7772  addnqprlemfu  7773  mulnqprlemfl  7788  mulnqprlemfu  7789  addcanprleml  7827  addcanprlemu  7828  cauappcvgprlemladdru  7869  cauappcvgprlemladdrl  7870  caucvgprlemladdrl  7891  caucvgprprlemaddq  7921  ltletr  8262  apreap  8760  ltleap  8805  uzm1  9780  xrltletr  10035  xaddf  10072  xaddval  10073  iseqf1olemqcl  10754  iseqf1olemnab  10756  iseqf1olemab  10757  exp3val  10796  zfz1isolemiso  11096  ltabs  11641  xrmaxiflemlub  11802  fprodsplitdc  12150  fprodcl2lem  12159  bitsfzo  12509  bezoutlemmain  12562  nninfctlemfo  12604  4sqlem17  12973  4sqlem18  12974  plycoeid3  15474  dvply1  15482  perfectlem2  15717  lgsval  15726  lgsfvalg  15727  lgsdilem  15749  lgsdir  15757  lgsabs1  15761  gausslemma2dlem1f1o  15782  lgseisenlem1  15792  2sqlem7  15843  clwwlknnn  16221  2omap  16544  nninfalllem1  16560  nninfall  16561  nninfsellemqall  16567  nninffeq  16572  nninfnfiinf  16575  trilpolemeq1  16594  nconstwlpolem  16619