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

Theorem ecased 1349
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 306 . 2  |-  ( ph  ->  ( -.  ch  /\  ( ps  \/  ch ) ) )
4 orel2 726 . . 3  |-  ( -. 
ch  ->  ( ( ps  \/  ch )  ->  ps ) )
54imp 124 . 2  |-  ( ( -.  ch  /\  ( ps  \/  ch ) )  ->  ps )
63, 5syl 14 1  |-  ( ph  ->  ps )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    \/ wo 708
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in2 615  ax-io 709
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ecase23d  1350  ontriexmidim  4520  preleq  4553  ordsuc  4561  reg3exmidlemwe  4577  sotri3  5026  diffisn  6890  onunsnss  6913  fival  6966  suplub2ti  6997  fodjum  7141  nninfwlpoimlemginf  7171  3nelsucpw1  7230  3nsssucpw1  7232  addnqprlemfl  7555  addnqprlemfu  7556  mulnqprlemfl  7571  mulnqprlemfu  7572  addcanprleml  7610  addcanprlemu  7611  cauappcvgprlemladdru  7652  cauappcvgprlemladdrl  7653  caucvgprlemladdrl  7674  caucvgprprlemaddq  7704  ltletr  8043  apreap  8540  ltleap  8585  uzm1  9554  xrltletr  9803  xaddf  9840  xaddval  9841  iseqf1olemqcl  10481  iseqf1olemnab  10483  iseqf1olemab  10484  exp3val  10517  zfz1isolemiso  10812  ltabs  11089  xrmaxiflemlub  11249  fprodsplitdc  11597  fprodcl2lem  11606  bezoutlemmain  11991  lgsval  14276  lgsfvalg  14277  lgsdilem  14299  lgsdir  14307  lgsabs1  14311  2sqlem7  14328  nninfalllem1  14617  nninfall  14618  nninfsellemqall  14624  nninffeq  14629  trilpolemeq1  14648  nconstwlpolem  14672
  Copyright terms: Public domain W3C validator