Theorem ecased 1362

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

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

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 616  ax-io 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1363  ontriexmidim  4575  preleq  4608  ordsuc  4616  reg3exmidlemwe  4632  sotri3  5087  pw2f1odclem  6943  diffisn  7002  onunsnss  7026  fival  7084  suplub2ti  7115  fodjum  7260  nninfwlpoimlemginf  7290  3nelsucpw1  7359  3nsssucpw1  7361  addnqprlemfl  7685  addnqprlemfu  7686  mulnqprlemfl  7701  mulnqprlemfu  7702  addcanprleml  7740  addcanprlemu  7741  cauappcvgprlemladdru  7782  cauappcvgprlemladdrl  7783  caucvgprlemladdrl  7804  caucvgprprlemaddq  7834  ltletr  8175  apreap  8673  ltleap  8718  uzm1  9692  xrltletr  9942  xaddf  9979  xaddval  9980  iseqf1olemqcl  10657  iseqf1olemnab  10659  iseqf1olemab  10660  exp3val  10699  zfz1isolemiso  10997  ltabs  11448  xrmaxiflemlub  11609  fprodsplitdc  11957  fprodcl2lem  11966  bitsfzo  12316  bezoutlemmain  12369  nninfctlemfo  12411  4sqlem17  12780  4sqlem18  12781  plycoeid3  15279  dvply1  15287  perfectlem2  15522  lgsval  15531  lgsfvalg  15532  lgsdilem  15554  lgsdir  15562  lgsabs1  15566  gausslemma2dlem1f1o  15587  lgseisenlem1  15597  2sqlem7  15648  2omap  16047  nninfalllem1  16060  nninfall  16061  nninfsellemqall  16067  nninffeq  16072  nninfnfiinf  16075  trilpolemeq1  16094  nconstwlpolem  16119