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  7139  diffisn  7202  onunsnss  7229  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  9970  xrltletr  10227  xaddf  10264  xaddval  10265  iseqf1olemqcl  10958  iseqf1olemnab  10960  iseqf1olemab  10961  exp3val  11000  zfz1isolemiso  11314  ltabs  11877  xrmaxiflemlub  12040  fprodsplitdc  12389  fprodcl2lem  12398  bitsfzo  12748  bezoutlemmain  12801  nninfctlemfo  12843  4sqlem17  13216  4sqlem18  13217  plycoeid3  15995  dvply1  16003  ppinprm  16272  chtnprm  16274  perfectlem2  16312  lgsval  16340  lgsfvalg  16341  lgsdilem  16363  lgsdir  16371  lgsabs1  16375  gausslemma2dlem1f1o  16396  lgseisenlem1  16406  2sqlem7  16457  clwwlknnn  16870  idjudju  17264  nninfalllem1  17269  nninfall  17270  nninfsellemqall  17276  nninffeq  17281  nninfnfiinf  17284  trilpolemeq1  17308  nconstwlpolem  17334