Theorem ecased 1390

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  ecase23d  1391  ecase2d  1392  rabsnif  3778  ontriexmidim  4669  preleq  4702  ordsuc  4710  reg3exmidlemwe  4726  sotri3  5186  pw2f1odclem  7134  diffisn  7197  onunsnss  7224  fival  7304  2omap  7319  suplub2ti  7342  fodjum  7487  nninfwlpoimlemginf  7517  3nelsucpw1  7594  3nsssucpw1  7596  addnqprlemfl  7927  addnqprlemfu  7928  mulnqprlemfl  7943  mulnqprlemfu  7944  addcanprleml  7982  addcanprlemu  7983  cauappcvgprlemladdru  8024  cauappcvgprlemladdrl  8025  caucvgprlemladdrl  8046  caucvgprprlemaddq  8076  ltletr  8416  apreap  8918  ltleap  8963  uzm1  9963  xrltletr  10220  xaddf  10257  xaddval  10258  iseqf1olemqcl  10950  iseqf1olemnab  10952  iseqf1olemab  10953  exp3val  10992  zfz1isolemiso  11306  ltabs  11869  xrmaxiflemlub  12032  fprodsplitdc  12381  fprodcl2lem  12390  bitsfzo  12740  bezoutlemmain  12793  nninfctlemfo  12835  4sqlem17  13208  4sqlem18  13209  plycoeid3  15910  dvply1  15918  ppinprm  16182  chtnprm  16184  perfectlem2  16222  lgsval  16245  lgsfvalg  16246  lgsdilem  16268  lgsdir  16276  lgsabs1  16280  gausslemma2dlem1f1o  16301  lgseisenlem1  16311  2sqlem7  16362  clwwlknnn  16775  nninfalllem1  17173  nninfall  17174  nninfsellemqall  17180  nninffeq  17185  nninfnfiinf  17188  trilpolemeq1  17211  nconstwlpolem  17237