MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orel2 Unicode version

Theorem orel2 383
Description: Elimination of disjunction by denial of a disjunct. Theorem *2.56 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 5-Apr-2013.)
Assertion
Ref Expression
orel2

Proof of Theorem orel2
StepHypRef Expression
1 idd 24 . 2
2 pm2.21 108 . 2
31, 2jaod 380 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368
This theorem is referenced by:  biorfi  407  pm2.64  789  pm2.74  846  pm5.71  936  prel12  4207  xpcan2  5449  funun  5635  ablfac1eulem  17123  drngmuleq0  17419  mdetunilem9  19122  maducoeval2  19142  tdeglem4  22458  deg1sublt  22511  dgrnznn  22644  dvply1  22680  aaliou2  22736  colline  24030  axcontlem2  24268  3orel3  29089  dfrdg4  29600  arg-ax  29881  elpell14qr2  30798  elpell1qr2  30808  jm2.22  30937  jm2.23  30938  jm2.26lem3  30943  ttac  30978  wepwsolem  30987  fmul01lt1lem2  31579  cncfiooicclem1  31696  3ornot23VD  33647
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370
  Copyright terms: Public domain W3C validator