Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  ecased 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  6540  addnqprlemfu  6541  addcanprleml  6588  addcanprlemu  6589  cauappcvgprlemladdru  6628  cauappcvgprlemladdrl  6629  caucvgprlemladdrl  6649  ltletr  6904  apreap  7371  ltleap  7413  uzm1  8279  xrltletr  8493
 Copyright terms: Public domain W3C validator