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  2213  prel12  3791  xpcan  5114  funun  5298  soxp  6230  sorpssuni  6288  sorpssint  6289  ackbij1lem18  7865  ackbij1b  7867  fincssdom  7951  fin23lem30  7970  fin1a2lem13  8040  pythagtriplem4  12874  zlpirlem3  16445  evlslem3  19400  3orel1  24063  3orel13  24073  dfon2lem4  24144  dfon2lem6  24146  dfrdg4  24490  rankeq1o  24803  pellfund14gap  26983  wepwsolem  27149  fmul01lt1lem1  27725
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