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

Theorem ecased 1238
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 290 . 2 (φ → (¬ χ (ψ χ)))
4 orel2 644 . . 3 χ → ((ψ χ) → ψ))
54imp 115 . 2 ((¬ χ (ψ χ)) → ψ)
63, 5syl 14 1 (φψ)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wa 97   wo 628
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in2 545  ax-io 629
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ecase23d  1239  preleq  4233  ordsuc  4241  sotri3  4666  addnqprlemfl  6539  addnqprlemfu  6540  addcanprleml  6587  addcanprlemu  6588  cauappcvgprlemladdru  6627  cauappcvgprlemladdrl  6628  ltletr  6884  apreap  7351  ltleap  7393  uzm1  8259  xrltletr  8473
  Copyright terms: Public domain W3C validator