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  2211  prel12  3789  xpcan  5112  funun  5296  soxp  6228  sorpssuni  6286  sorpssint  6287  ackbij1lem18  7863  ackbij1b  7865  fincssdom  7949  fin23lem30  7968  fin1a2lem13  8038  pythagtriplem4  12872  zlpirlem3  16443  evlslem3  19398  3orel1  24061  3orel13  24071  dfon2lem4  24142  dfon2lem6  24144  dfrdg4  24488  rankeq1o  24801  pellfund14gap  26972  wepwsolem  27138  fmul01lt1lem1  27714
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