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  4671  preleq  4704  ordsuc  4712  reg3exmidlemwe  4728  sotri3  5189  pw2f1odclem  7140  diffisn  7203  onunsnss  7230  fival  7310  2omap  7325  suplub2ti  7348  fodjum  7493  nninfwlpoimlemginf  7523  3nelsucpw1  7600  3nsssucpw1  7602  addnqprlemfl  7933  addnqprlemfu  7934  mulnqprlemfl  7949  mulnqprlemfu  7950  addcanprleml  7988  addcanprlemu  7989  cauappcvgprlemladdru  8030  cauappcvgprlemladdrl  8031  caucvgprlemladdrl  8052  caucvgprprlemaddq  8082  ltletr  8422  apreap  8924  ltleap  8969  uzm1  9969  xrltletr  10226  xaddf  10263  xaddval  10264  iseqf1olemqcl  10957  iseqf1olemnab  10959  iseqf1olemab  10960  exp3val  10999  zfz1isolemiso  11313  ltabs  11876  xrmaxiflemlub  12039  fprodsplitdc  12388  fprodcl2lem  12397  bitsfzo  12747  bezoutlemmain  12800  nninfctlemfo  12842  4sqlem17  13215  4sqlem18  13216  plycoeid3  16016  dvply1  16024  ppinprm  16293  chtnprm  16295  perfectlem2  16333  lgsval  16361  lgsfvalg  16362  lgsdilem  16384  lgsdir  16392  lgsabs1  16396  gausslemma2dlem1f1o  16417  lgseisenlem1  16427  2sqlem7  16478  clwwlknnn  16891  idjudju  17285  nninfalllem1  17290  nninfall  17291  nninfsellemqall  17297  nninffeq  17302  nninfnfiinf  17305  trilpolemeq1  17329  nconstwlpolem  17355