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

Theorem orel1 373
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 364 . 2  |-  ( (
ph  \/  ps )  ->  ( -.  ph  ->  ps ) )
21com12 29 1  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6    \/ wo 359
This theorem is referenced by:  pm2.25  395  biorf  396  euor2  2184  prel12  3730  xpcan  5065  funun  5199  soxp  6127  sorpssuni  6185  sorpssint  6186  ackbij1lem18  7796  ackbij1b  7798  fincssdom  7882  fin23lem30  7901  fin1a2lem13  7971  pythagtriplem4  12799  zlpirlem3  16370  evlslem3  19325  3orel1  23398  3orel13  23408  dfon2lem4  23476  dfon2lem6  23478  dfrdg4  23828  rankeq1o  24141  pellfund14gap  26304  wepwsolem  26470  fmul01lt1lem1  27047
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
This theorem depends on definitions:  df-bi 179  df-or 361
  Copyright terms: Public domain W3C validator