Theorem ecased 1362

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

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1363  ontriexmidim  4578  preleq  4611  ordsuc  4619  reg3exmidlemwe  4635  sotri3  5090  pw2f1odclem  6946  diffisn  7005  onunsnss  7029  fival  7087  suplub2ti  7118  fodjum  7263  nninfwlpoimlemginf  7293  3nelsucpw1  7365  3nsssucpw1  7367  addnqprlemfl  7692  addnqprlemfu  7693  mulnqprlemfl  7708  mulnqprlemfu  7709  addcanprleml  7747  addcanprlemu  7748  cauappcvgprlemladdru  7789  cauappcvgprlemladdrl  7790  caucvgprlemladdrl  7811  caucvgprprlemaddq  7841  ltletr  8182  apreap  8680  ltleap  8725  uzm1  9699  xrltletr  9949  xaddf  9986  xaddval  9987  iseqf1olemqcl  10666  iseqf1olemnab  10668  iseqf1olemab  10669  exp3val  10708  zfz1isolemiso  11006  ltabs  11473  xrmaxiflemlub  11634  fprodsplitdc  11982  fprodcl2lem  11991  bitsfzo  12341  bezoutlemmain  12394  nninfctlemfo  12436  4sqlem17  12805  4sqlem18  12806  plycoeid3  15304  dvply1  15312  perfectlem2  15547  lgsval  15556  lgsfvalg  15557  lgsdilem  15579  lgsdir  15587  lgsabs1  15591  gausslemma2dlem1f1o  15612  lgseisenlem1  15622  2sqlem7  15673  2omap  16071  nninfalllem1  16086  nninfall  16087  nninfsellemqall  16093  nninffeq  16098  nninfnfiinf  16101  trilpolemeq1  16120  nconstwlpolem  16145