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

Theorem ecased 1328
 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 304 . 2
4 orel2 716 . . 3
54imp 123 . 2
63, 5syl 14 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wa 103   wo 698 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in2 605  ax-io 699 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  ecase23d  1329  ontriexmidim  4475  preleq  4508  ordsuc  4516  reg3exmidlemwe  4532  sotri3  4977  diffisn  6827  onunsnss  6850  fival  6903  suplub2ti  6933  fodjum  7068  3nelsucpw1  7148  3nsssucpw1  7150  addnqprlemfl  7458  addnqprlemfu  7459  mulnqprlemfl  7474  mulnqprlemfu  7475  addcanprleml  7513  addcanprlemu  7514  cauappcvgprlemladdru  7555  cauappcvgprlemladdrl  7556  caucvgprlemladdrl  7577  caucvgprprlemaddq  7607  ltletr  7945  apreap  8441  ltleap  8486  uzm1  9448  xrltletr  9689  xaddf  9726  xaddval  9727  iseqf1olemqcl  10363  iseqf1olemnab  10365  iseqf1olemab  10366  exp3val  10399  zfz1isolemiso  10687  ltabs  10964  xrmaxiflemlub  11122  fprodsplitdc  11470  fprodcl2lem  11479  bezoutlemmain  11853  nninfalllem1  13521  nninfall  13522  nninfsellemqall  13528  nninffeq  13533  trilpolemeq1  13552  nconstwlpolem  13576
 Copyright terms: Public domain W3C validator