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

Theorem orel1 371
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  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )

Proof of Theorem orel1
StepHypRef Expression
1 pm2.53 362 . 2  |-  ( (
ph  \/  ps )  ->  ( -.  ph  ->  ps ) )
21com12 27 1  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357
This theorem is referenced by:  pm2.25  393  biorf  394  euor2  2277  prel12  3870  xpcan  5194  funun  5378  soxp  6315  sorpssuni  6373  sorpssint  6374  ackbij1lem18  7953  ackbij1b  7955  fincssdom  8039  fin23lem30  8058  fin1a2lem13  8128  pythagtriplem4  12969  zlpirlem3  16549  evlslem3  19502  elzdif0  23637  qqhval2lem  23638  3orel1  24465  3orel13  24475  dfon2lem4  24700  dfon2lem6  24702  dfrdg4  25047  rankeq1o  25360  pellfund14gap  26295  wepwsolem  26461  fmul01lt1lem1  27037
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator