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  2212  prel12  3790  xpcan  5111  funun  5262  soxp  6190  sorpssuni  6248  sorpssint  6249  ackbij1lem18  7859  ackbij1b  7861  fincssdom  7945  fin23lem30  7964  fin1a2lem13  8034  pythagtriplem4  12868  zlpirlem3  16439  evlslem3  19394  3orel1  23468  3orel13  23478  dfon2lem4  23546  dfon2lem6  23548  dfrdg4  23898  rankeq1o  24211  pellfund14gap  26383  wepwsolem  26549  fmul01lt1lem1  27125
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