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  3763  ontriexmidim  4649  preleq  4682  ordsuc  4690  reg3exmidlemwe  4706  sotri3  5166  pw2f1odclem  7100  diffisn  7163  onunsnss  7190  fival  7270  2omap  7282  suplub2ti  7305  fodjum  7450  nninfwlpoimlemginf  7480  3nelsucpw1  7557  3nsssucpw1  7559  addnqprlemfl  7890  addnqprlemfu  7891  mulnqprlemfl  7906  mulnqprlemfu  7907  addcanprleml  7945  addcanprlemu  7946  cauappcvgprlemladdru  7987  cauappcvgprlemladdrl  7988  caucvgprlemladdrl  8009  caucvgprprlemaddq  8039  ltletr  8379  apreap  8878  ltleap  8923  uzm1  9903  xrltletr  10159  xaddf  10196  xaddval  10197  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemab  10888  exp3val  10927  zfz1isolemiso  11236  ltabs  11797  xrmaxiflemlub  11958  fprodsplitdc  12307  fprodcl2lem  12316  bitsfzo  12666  bezoutlemmain  12719  nninfctlemfo  12761  4sqlem17  13130  4sqlem18  13131  plycoeid3  15734  dvply1  15742  perfectlem2  15980  lgsval  15989  lgsfvalg  15990  lgsdilem  16012  lgsdir  16020  lgsabs1  16024  gausslemma2dlem1f1o  16045  lgseisenlem1  16055  2sqlem7  16106  clwwlknnn  16519  nninfalllem1  16898  nninfall  16899  nninfsellemqall  16905  nninffeq  16910  nninfnfiinf  16913  trilpolemeq1  16936  nconstwlpolem  16963