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  4614  preleq  4647  ordsuc  4655  reg3exmidlemwe  4671  sotri3  5127  pw2f1odclem  7003  diffisn  7063  onunsnss  7087  fival  7145  suplub2ti  7176  fodjum  7321  nninfwlpoimlemginf  7351  3nelsucpw1  7427  3nsssucpw1  7429  addnqprlemfl  7754  addnqprlemfu  7755  mulnqprlemfl  7770  mulnqprlemfu  7771  addcanprleml  7809  addcanprlemu  7810  cauappcvgprlemladdru  7851  cauappcvgprlemladdrl  7852  caucvgprlemladdrl  7873  caucvgprprlemaddq  7903  ltletr  8244  apreap  8742  ltleap  8787  uzm1  9761  xrltletr  10011  xaddf  10048  xaddval  10049  iseqf1olemqcl  10729  iseqf1olemnab  10731  iseqf1olemab  10732  exp3val  10771  zfz1isolemiso  11069  ltabs  11606  xrmaxiflemlub  11767  fprodsplitdc  12115  fprodcl2lem  12124  bitsfzo  12474  bezoutlemmain  12527  nninfctlemfo  12569  4sqlem17  12938  4sqlem18  12939  plycoeid3  15439  dvply1  15447  perfectlem2  15682  lgsval  15691  lgsfvalg  15692  lgsdilem  15714  lgsdir  15722  lgsabs1  15726  gausslemma2dlem1f1o  15747  lgseisenlem1  15757  2sqlem7  15808  2omap  16388  nninfalllem1  16404  nninfall  16405  nninfsellemqall  16411  nninffeq  16416  nninfnfiinf  16419  trilpolemeq1  16438  nconstwlpolem  16463