Theorem ecased 1360

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1361  ontriexmidim  4559  preleq  4592  ordsuc  4600  reg3exmidlemwe  4616  sotri3  5069  pw2f1odclem  6904  diffisn  6963  onunsnss  6987  fival  7045  suplub2ti  7076  fodjum  7221  nninfwlpoimlemginf  7251  3nelsucpw1  7317  3nsssucpw1  7319  addnqprlemfl  7643  addnqprlemfu  7644  mulnqprlemfl  7659  mulnqprlemfu  7660  addcanprleml  7698  addcanprlemu  7699  cauappcvgprlemladdru  7740  cauappcvgprlemladdrl  7741  caucvgprlemladdrl  7762  caucvgprprlemaddq  7792  ltletr  8133  apreap  8631  ltleap  8676  uzm1  9649  xrltletr  9899  xaddf  9936  xaddval  9937  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemab  10611  exp3val  10650  zfz1isolemiso  10948  ltabs  11269  xrmaxiflemlub  11430  fprodsplitdc  11778  fprodcl2lem  11787  bitsfzo  12137  bezoutlemmain  12190  nninfctlemfo  12232  4sqlem17  12601  4sqlem18  12602  plycoeid3  15077  dvply1  15085  perfectlem2  15320  lgsval  15329  lgsfvalg  15330  lgsdilem  15352  lgsdir  15360  lgsabs1  15364  gausslemma2dlem1f1o  15385  lgseisenlem1  15395  2sqlem7  15446  2omap  15726  nninfalllem1  15739  nninfall  15740  nninfsellemqall  15746  nninffeq  15751  trilpolemeq1  15771  nconstwlpolem  15796