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  4558  preleq  4591  ordsuc  4599  reg3exmidlemwe  4615  sotri3  5068  pw2f1odclem  6895  diffisn  6954  onunsnss  6978  fival  7036  suplub2ti  7067  fodjum  7212  nninfwlpoimlemginf  7242  3nelsucpw1  7301  3nsssucpw1  7303  addnqprlemfl  7626  addnqprlemfu  7627  mulnqprlemfl  7642  mulnqprlemfu  7643  addcanprleml  7681  addcanprlemu  7682  cauappcvgprlemladdru  7723  cauappcvgprlemladdrl  7724  caucvgprlemladdrl  7745  caucvgprprlemaddq  7775  ltletr  8116  apreap  8614  ltleap  8659  uzm1  9632  xrltletr  9882  xaddf  9919  xaddval  9920  iseqf1olemqcl  10591  iseqf1olemnab  10593  iseqf1olemab  10594  exp3val  10633  zfz1isolemiso  10931  ltabs  11252  xrmaxiflemlub  11413  fprodsplitdc  11761  fprodcl2lem  11770  bitsfzo  12119  bezoutlemmain  12165  nninfctlemfo  12207  4sqlem17  12576  4sqlem18  12577  plycoeid3  14993  dvply1  15001  perfectlem2  15236  lgsval  15245  lgsfvalg  15246  lgsdilem  15268  lgsdir  15276  lgsabs1  15280  gausslemma2dlem1f1o  15301  lgseisenlem1  15311  2sqlem7  15362  nninfalllem1  15652  nninfall  15653  nninfsellemqall  15659  nninffeq  15664  trilpolemeq1  15684  nconstwlpolem  15709