Theorem ecased 1390

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 104   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 624  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  ecase23d  1391  ecase2d  1392  rabsnif  3778  ontriexmidim  4669  preleq  4702  ordsuc  4710  reg3exmidlemwe  4726  sotri3  5186  pw2f1odclem  7134  diffisn  7197  onunsnss  7224  fival  7304  2omap  7318  suplub2ti  7341  fodjum  7486  nninfwlpoimlemginf  7516  3nelsucpw1  7593  3nsssucpw1  7595  addnqprlemfl  7926  addnqprlemfu  7927  mulnqprlemfl  7942  mulnqprlemfu  7943  addcanprleml  7981  addcanprlemu  7982  cauappcvgprlemladdru  8023  cauappcvgprlemladdrl  8024  caucvgprlemladdrl  8045  caucvgprprlemaddq  8075  ltletr  8415  apreap  8916  ltleap  8961  uzm1  9955  xrltletr  10211  xaddf  10248  xaddval  10249  iseqf1olemqcl  10938  iseqf1olemnab  10940  iseqf1olemab  10941  exp3val  10980  zfz1isolemiso  11293  ltabs  11855  xrmaxiflemlub  12016  fprodsplitdc  12365  fprodcl2lem  12374  bitsfzo  12724  bezoutlemmain  12777  nninfctlemfo  12819  4sqlem17  13188  4sqlem18  13189  plycoeid3  15860  dvply1  15868  perfectlem2  16120  lgsval  16135  lgsfvalg  16136  lgsdilem  16158  lgsdir  16166  lgsabs1  16170  gausslemma2dlem1f1o  16191  lgseisenlem1  16201  2sqlem7  16252  clwwlknnn  16665  nninfalllem1  17063  nninfall  17064  nninfsellemqall  17070  nninffeq  17075  nninfnfiinf  17078  trilpolemeq1  17101  nconstwlpolem  17127