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

Theorem ecased 1239
Description: Deduction form of disjunctive syllogism. (Contributed by Jim Kingdon, 9-Dec-2017.)
Hypotheses
Ref Expression
ecased.1  |-  ( ph  ->  -.  ch )
ecased.2  |-  ( ph  ->  ( ps  \/  ch ) )
Assertion
Ref Expression
ecased  |-  ( ph  ->  ps )

Proof of Theorem ecased
StepHypRef Expression
1 ecased.1 . . 3  |-  ( ph  ->  -.  ch )
2 ecased.2 . . 3  |-  ( ph  ->  ( ps  \/  ch ) )
31, 2jca 290 . 2  |-  ( ph  ->  ( -.  ch  /\  ( ps  \/  ch ) ) )
4 orel2 645 . . 3  |-  ( -. 
ch  ->  ( ( ps  \/  ch )  ->  ps ) )
54imp 115 . 2  |-  ( ( -.  ch  /\  ( ps  \/  ch ) )  ->  ps )
63, 5syl 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 97    \/ wo 629
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 630
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ecase23d  1240  preleq  4279  ordsuc  4287  reg3exmidlemwe  4303  sotri3  4723  diffisn  6350  onunsnss  6355  addnqprlemfl  6657  addnqprlemfu  6658  mulnqprlemfl  6673  mulnqprlemfu  6674  addcanprleml  6712  addcanprlemu  6713  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprlemladdrl  6776  caucvgprprlemaddq  6806  ltletr  7107  apreap  7578  ltleap  7621  uzm1  8503  xrltletr  8723  ltabs  9683
  Copyright terms: Public domain W3C validator