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  2224  prel12  3805  xpcan  5128  funun  5312  soxp  6244  sorpssuni  6302  sorpssint  6303  ackbij1lem18  7879  ackbij1b  7881  fincssdom  7965  fin23lem30  7984  fin1a2lem13  8054  pythagtriplem4  12888  zlpirlem3  16459  evlslem3  19414  3orel1  24076  3orel13  24086  dfon2lem4  24213  dfon2lem6  24215  dfrdg4  24560  rankeq1o  24873  pellfund14gap  27075  wepwsolem  27241  fmul01lt1lem1  27817
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