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

Theorem orel1 380
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 371 . 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 366
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 368
This theorem is referenced by:  pm2.25  402  biorf  403  ornldOLD  897  prel12  4121  xpcan  5353  funun  5538  sorpssuni  6488  sorpssint  6489  soxp  6812  ackbij1lem18  8530  ackbij1b  8532  fincssdom  8616  fin23lem30  8635  fin1a2lem13  8705  pythagtriplem4  14345  evlslem3  18296  zringlpirlem3  18617  psgnodpm  18715  orngsqr  27948  elzdif0  28114  qqhval2lem  28115  eulerpartlemsv2  28480  eulerpartlemv  28486  eulerpartlemf  28492  eulerpartlemgh  28500  3orel1  29253  3orel13  29260  dfon2lem4  29383  dfon2lem6  29385  dfrdg4  29753  rankeq1o  29981  wl-orel12  30134  pellfund14gap  30988  wepwsolem  31153  fmul01lt1lem1  31744  cncfiooicclem1  31862  etransclem24  32207
  Copyright terms: Public domain W3C validator