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

Theorem ecased 1255
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 294 . 2  |-  ( ph  ->  ( -.  ch  /\  ( ps  \/  ch ) ) )
4 orel2 655 . . 3  |-  ( -. 
ch  ->  ( ( ps  \/  ch )  ->  ps ) )
54imp 119 . 2  |-  ( ( -.  ch  /\  ( ps  \/  ch ) )  ->  ps )
63, 5syl 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 101    \/ wo 639
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in2 555  ax-io 640
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  ecase23d  1256  preleq  4307  ordsuc  4315  reg3exmidlemwe  4331  sotri3  4751  diffisn  6381  onunsnss  6386  addnqprlemfl  6715  addnqprlemfu  6716  mulnqprlemfl  6731  mulnqprlemfu  6732  addcanprleml  6770  addcanprlemu  6771  cauappcvgprlemladdru  6812  cauappcvgprlemladdrl  6813  caucvgprlemladdrl  6834  caucvgprprlemaddq  6864  ltletr  7166  apreap  7652  ltleap  7695  uzm1  8599  xrltletr  8824  ltabs  9914
  Copyright terms: Public domain W3C validator