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  7319  3nsssucpw1  7321  addnqprlemfl  7645  addnqprlemfu  7646  mulnqprlemfl  7661  mulnqprlemfu  7662  addcanprleml  7700  addcanprlemu  7701  cauappcvgprlemladdru  7742  cauappcvgprlemladdrl  7743  caucvgprlemladdrl  7764  caucvgprprlemaddq  7794  ltletr  8135  apreap  8633  ltleap  8678  uzm1  9651  xrltletr  9901  xaddf  9938  xaddval  9939  iseqf1olemqcl  10610  iseqf1olemnab  10612  iseqf1olemab  10613  exp3val  10652  zfz1isolemiso  10950  ltabs  11271  xrmaxiflemlub  11432  fprodsplitdc  11780  fprodcl2lem  11789  bitsfzo  12139  bezoutlemmain  12192  nninfctlemfo  12234  4sqlem17  12603  4sqlem18  12604  plycoeid3  15101  dvply1  15109  perfectlem2  15344  lgsval  15353  lgsfvalg  15354  lgsdilem  15376  lgsdir  15384  lgsabs1  15388  gausslemma2dlem1f1o  15409  lgseisenlem1  15419  2sqlem7  15470  2omap  15750  nninfalllem1  15763  nninfall  15764  nninfsellemqall  15770  nninffeq  15775  nninfnfiinf  15778  trilpolemeq1  15797  nconstwlpolem  15822