MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orel1 Structured version   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  2349  prel12  3975  xpcan  5305  funun  5495  soxp  6459  sorpssuni  6531  sorpssint  6532  ackbij1lem18  8117  ackbij1b  8119  fincssdom  8203  fin23lem30  8222  fin1a2lem13  8292  pythagtriplem4  13193  zlpirlem3  16770  evlslem3  19935  ofldsqr  24240  elzdif0  24364  qqhval2lem  24365  3orel1  25164  3orel13  25174  dfon2lem4  25413  dfon2lem6  25415  dfrdg4  25795  rankeq1o  26112  pellfund14gap  26950  wepwsolem  27116  fmul01lt1lem1  27690
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