Theorem ecased 1349

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

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

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 615  ax-io 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ecase23d  1350  ontriexmidim  4515  preleq  4548  ordsuc  4556  reg3exmidlemwe  4572  sotri3  5019  diffisn  6883  onunsnss  6906  fival  6959  suplub2ti  6990  fodjum  7134  nninfwlpoimlemginf  7164  3nelsucpw1  7223  3nsssucpw1  7225  addnqprlemfl  7533  addnqprlemfu  7534  mulnqprlemfl  7549  mulnqprlemfu  7550  addcanprleml  7588  addcanprlemu  7589  cauappcvgprlemladdru  7630  cauappcvgprlemladdrl  7631  caucvgprlemladdrl  7652  caucvgprprlemaddq  7682  ltletr  8021  apreap  8518  ltleap  8563  uzm1  9529  xrltletr  9776  xaddf  9813  xaddval  9814  iseqf1olemqcl  10454  iseqf1olemnab  10456  iseqf1olemab  10457  exp3val  10490  zfz1isolemiso  10785  ltabs  11062  xrmaxiflemlub  11222  fprodsplitdc  11570  fprodcl2lem  11579  bezoutlemmain  11964  lgsval  13956  lgsfvalg  13957  lgsdilem  13979  lgsdir  13987  lgsabs1  13991  2sqlem7  14008  nninfalllem1  14298  nninfall  14299  nninfsellemqall  14305  nninffeq  14310  trilpolemeq1  14329  nconstwlpolem  14353