ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ecased GIF version

Theorem ecased 1283
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
StepHypRef Expression
1 ecased.1 . . 3 (𝜑 → ¬ 𝜒)
2 ecased.2 . . 3 (𝜑 → (𝜓𝜒))
31, 2jca 300 . 2 (𝜑 → (¬ 𝜒 ∧ (𝜓𝜒)))
4 orel2 678 . . 3 𝜒 → ((𝜓𝜒) → 𝜓))
54imp 122 . 2 ((¬ 𝜒 ∧ (𝜓𝜒)) → 𝜓)
63, 5syl 14 1 (𝜑𝜓)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in2 578  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  ecase23d  1284  preleq  4337  ordsuc  4345  reg3exmidlemwe  4360  sotri3  4788  diffisn  6542  onunsnss  6557  suplub2ti  6617  fodjuomnilemm  6722  addnqprlemfl  7039  addnqprlemfu  7040  mulnqprlemfl  7055  mulnqprlemfu  7056  addcanprleml  7094  addcanprlemu  7095  cauappcvgprlemladdru  7136  cauappcvgprlemladdrl  7137  caucvgprlemladdrl  7158  caucvgprprlemaddq  7188  ltletr  7495  apreap  7982  ltleap  8025  uzm1  8958  xrltletr  9181  ltabs  10361  bezoutlemmain  10781  nninfalllem1  11255  nninfall  11256  nninfsellemqall  11263
  Copyright terms: Public domain W3C validator