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

Theorem orel1 382
Description: Elimination of disjunction by denial of a disjunct. Theorem *2.55 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 21-Jul-2012.)
Assertion
Ref Expression
orel1

Proof of Theorem orel1
StepHypRef Expression
1 pm2.53 373 . 2
21com12 31 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  \/wo 368
This theorem is referenced by:  pm2.25  404  biorf  405  euor2OLD  2322  prel12  4166  xpcan  5393  funun  5579  sorpssuni  6502  sorpssint  6503  soxp  6819  ackbij1lem18  8543  ackbij1b  8545  fincssdom  8629  fin23lem30  8648  fin1a2lem13  8718  pythagtriplem4  14044  evlslem3  17777  zringlpirlem3  18098  zlpirlem3  18103  psgnodpm  18211  orngsqr  26729  elzdif0  26866  qqhval2lem  26867  eulerpartlemsv2  27197  eulerpartlemv  27203  eulerpartlemf  27209  eulerpartlemgh  27217  3orel1  27822  3orel13  27829  dfon2lem4  28055  dfon2lem6  28057  dfrdg4  28437  rankeq1o  28665  pellfund14gap  29688  wepwsolem  29854  fmul01lt1lem1  30363  cncfiooicclem1  30461  ornld  30991
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