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

Theorem orel1 372
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 363 . 2  |-  ( (
ph  \/  ps )  ->  ( -.  ph  ->  ps ) )
21com12 29 1  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 358
This theorem is referenced by:  pm2.25  394  biorf  395  euor2  2322  prel12  3935  xpcan  5264  funun  5454  soxp  6418  sorpssuni  6490  sorpssint  6491  ackbij1lem18  8073  ackbij1b  8075  fincssdom  8159  fin23lem30  8178  fin1a2lem13  8248  pythagtriplem4  13148  zlpirlem3  16725  evlslem3  19888  ofldsqr  24193  elzdif0  24317  qqhval2lem  24318  3orel1  25117  3orel13  25127  dfon2lem4  25356  dfon2lem6  25358  dfrdg4  25703  rankeq1o  26016  pellfund14gap  26840  wepwsolem  27006  fmul01lt1lem1  27581
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 178  df-or 360
  Copyright terms: Public domain W3C validator