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  4555  preleq  4588  ordsuc  4596  reg3exmidlemwe  4612  sotri3  5065  pw2f1odclem  6892  diffisn  6951  onunsnss  6975  fival  7031  suplub2ti  7062  fodjum  7207  nninfwlpoimlemginf  7237  3nelsucpw1  7296  3nsssucpw1  7298  addnqprlemfl  7621  addnqprlemfu  7622  mulnqprlemfl  7637  mulnqprlemfu  7638  addcanprleml  7676  addcanprlemu  7677  cauappcvgprlemladdru  7718  cauappcvgprlemladdrl  7719  caucvgprlemladdrl  7740  caucvgprprlemaddq  7770  ltletr  8111  apreap  8608  ltleap  8653  uzm1  9626  xrltletr  9876  xaddf  9913  xaddval  9914  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemab  10576  exp3val  10615  zfz1isolemiso  10913  ltabs  11234  xrmaxiflemlub  11394  fprodsplitdc  11742  fprodcl2lem  11751  bezoutlemmain  12138  nninfctlemfo  12180  4sqlem17  12548  4sqlem18  12549  dvply1  14943  lgsval  15161  lgsfvalg  15162  lgsdilem  15184  lgsdir  15192  lgsabs1  15196  gausslemma2dlem1f1o  15217  lgseisenlem1  15227  2sqlem7  15278  nninfalllem1  15568  nninfall  15569  nninfsellemqall  15575  nninffeq  15580  trilpolemeq1  15600  nconstwlpolem  15625