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  2186  prel12  3763  xpcan  5100  funun  5234  soxp  6162  sorpssuni  6220  sorpssint  6221  ackbij1lem18  7831  ackbij1b  7833  fincssdom  7917  fin23lem30  7936  fin1a2lem13  8006  pythagtriplem4  12835  zlpirlem3  16406  evlslem3  19361  3orel1  23434  3orel13  23444  dfon2lem4  23512  dfon2lem6  23514  dfrdg4  23864  rankeq1o  24177  pellfund14gap  26340  wepwsolem  26506  fmul01lt1lem1  27083
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