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  2181  prel12  3689  xpcan  5019  funun  5153  soxp  6080  sorpssuni  6138  sorpssint  6139  ackbij1lem18  7747  ackbij1b  7749  fincssdom  7833  fin23lem30  7852  fin1a2lem13  7922  pythagtriplem4  12746  zlpirlem3  16275  evlslem3  19230  3orel1  23232  3orel13  23242  dfon2lem4  23310  dfon2lem6  23312  dfrdg4  23662  rankeq1o  23975  pellfund14gap  26138  wepwsolem  26304
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