Theorem ecased 1238

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 290	. 2 ⊢ (φ → (¬ χ ∧ (ψ ∨ χ)))
4		orel2 644	. . 3 ⊢ (¬ χ → ((ψ ∨ χ) → ψ))
5	4	imp 115	. 2 ⊢ ((¬ χ ∧ (ψ ∨ χ)) → ψ)
6	3, 5	syl 14	1 ⊢ (φ → ψ)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 97   ∨ wo 628

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in2 545  ax-io 629

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  ecase23d  1239  preleq  4233  ordsuc  4241  sotri3  4666  addnqprlemfl  6540  addnqprlemfu  6541  addcanprleml  6588  addcanprlemu  6589  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemladdrl  6649  ltletr  6904  apreap  7371  ltleap  7413  uzm1  8279  xrltletr  8493