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

Theorem orel1 382
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 373 . 2  |-  ( (
ph  \/  ps )  ->  ( -.  ph  ->  ps ) )
21com12 31 1  |-  ( -. 
ph  ->  ( ( ph  \/  ps )  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 368
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-or 370
This theorem is referenced by:  pm2.25  404  biorf  405  ornldOLD  899  prel12  4192  xpcan  5433  funun  5620  sorpssuni  6574  sorpssint  6575  soxp  6898  ackbij1lem18  8620  ackbij1b  8622  fincssdom  8706  fin23lem30  8725  fin1a2lem13  8795  pythagtriplem4  14220  evlslem3  18057  zringlpirlem3  18384  zlpirlem3  18389  psgnodpm  18497  orngsqr  27667  elzdif0  27834  qqhval2lem  27835  eulerpartlemsv2  28170  eulerpartlemv  28176  eulerpartlemf  28182  eulerpartlemgh  28190  3orel1  28960  3orel13  28967  dfon2lem4  29193  dfon2lem6  29195  dfrdg4  29575  rankeq1o  29803  pellfund14gap  30798  wepwsolem  30962  fmul01lt1lem1  31506  cncfiooicclem1  31603
  Copyright terms: Public domain W3C validator