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  4615  preleq  4648  ordsuc  4656  reg3exmidlemwe  4672  sotri3  5130  pw2f1odclem  7008  diffisn  7068  onunsnss  7095  fival  7153  suplub2ti  7184  fodjum  7329  nninfwlpoimlemginf  7359  3nelsucpw1  7435  3nsssucpw1  7437  addnqprlemfl  7762  addnqprlemfu  7763  mulnqprlemfl  7778  mulnqprlemfu  7779  addcanprleml  7817  addcanprlemu  7818  cauappcvgprlemladdru  7859  cauappcvgprlemladdrl  7860  caucvgprlemladdrl  7881  caucvgprprlemaddq  7911  ltletr  8252  apreap  8750  ltleap  8795  uzm1  9770  xrltletr  10020  xaddf  10057  xaddval  10058  iseqf1olemqcl  10738  iseqf1olemnab  10740  iseqf1olemab  10741  exp3val  10780  zfz1isolemiso  11079  ltabs  11619  xrmaxiflemlub  11780  fprodsplitdc  12128  fprodcl2lem  12137  bitsfzo  12487  bezoutlemmain  12540  nninfctlemfo  12582  4sqlem17  12951  4sqlem18  12952  plycoeid3  15452  dvply1  15460  perfectlem2  15695  lgsval  15704  lgsfvalg  15705  lgsdilem  15727  lgsdir  15735  lgsabs1  15739  gausslemma2dlem1f1o  15760  lgseisenlem1  15770  2sqlem7  15821  clwwlknnn  16181  2omap  16472  nninfalllem1  16488  nninfall  16489  nninfsellemqall  16495  nninffeq  16500  nninfnfiinf  16503  trilpolemeq1  16522  nconstwlpolem  16547