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  euor2OLD  2320  prel12  4150  xpcan  5375  funun  5561  sorpssuni  6472  sorpssint  6473  soxp  6788  ackbij1lem18  8510  ackbij1b  8512  fincssdom  8596  fin23lem30  8615  fin1a2lem13  8685  pythagtriplem4  13997  evlslem3  17716  zringlpirlem3  18023  zlpirlem3  18028  psgnodpm  18136  orngsqr  26410  elzdif0  26547  qqhval2lem  26548  eulerpartlemsv2  26878  eulerpartlemv  26884  eulerpartlemf  26890  eulerpartlemgh  26898  3orel1  27503  3orel13  27510  dfon2lem4  27736  dfon2lem6  27738  dfrdg4  28118  rankeq1o  28346  pellfund14gap  29369  wepwsolem  29535  fmul01lt1lem1  29906  ornld  30255
  Copyright terms: Public domain W3C validator