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  3749  xpcan  5086  funun  5220  soxp  6148  sorpssuni  6206  sorpssint  6207  ackbij1lem18  7817  ackbij1b  7819  fincssdom  7903  fin23lem30  7922  fin1a2lem13  7992  pythagtriplem4  12820  zlpirlem3  16391  evlslem3  19346  3orel1  23419  3orel13  23429  dfon2lem4  23497  dfon2lem6  23499  dfrdg4  23849  rankeq1o  24162  pellfund14gap  26325  wepwsolem  26491  fmul01lt1lem1  27068
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