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

Theorem ecased 1327
 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 304 . 2 (𝜑 → (¬ 𝜒 ∧ (𝜓𝜒)))
4 orel2 715 . . 3 𝜒 → ((𝜓𝜒) → 𝜓))
54imp 123 . 2 ((¬ 𝜒 ∧ (𝜓𝜒)) → 𝜓)
63, 5syl 14 1 (𝜑𝜓)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ∨ wo 697 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 604  ax-io 698 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  ecase23d  1328  preleq  4470  ordsuc  4478  reg3exmidlemwe  4493  sotri3  4937  diffisn  6787  onunsnss  6805  fival  6858  suplub2ti  6888  fodjum  7018  addnqprlemfl  7374  addnqprlemfu  7375  mulnqprlemfl  7390  mulnqprlemfu  7391  addcanprleml  7429  addcanprlemu  7430  cauappcvgprlemladdru  7471  cauappcvgprlemladdrl  7472  caucvgprlemladdrl  7493  caucvgprprlemaddq  7523  ltletr  7860  apreap  8356  ltleap  8401  uzm1  9363  xrltletr  9597  xaddf  9634  xaddval  9635  iseqf1olemqcl  10266  iseqf1olemnab  10268  iseqf1olemab  10269  exp3val  10302  zfz1isolemiso  10589  ltabs  10866  xrmaxiflemlub  11024  bezoutlemmain  11693  nninfalllem1  13217  nninfall  13218  nninfsellemqall  13225  nninffeq  13230  trilpolemeq1  13247
 Copyright terms: Public domain W3C validator