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  ornld  894  euor2OLD  2328  prel12  4196  xpcan  5434  funun  5621  sorpssuni  6564  sorpssint  6565  soxp  6886  ackbij1lem18  8606  ackbij1b  8608  fincssdom  8692  fin23lem30  8711  fin1a2lem13  8781  pythagtriplem4  14191  evlslem3  17947  zringlpirlem3  18271  zlpirlem3  18276  psgnodpm  18384  orngsqr  27443  elzdif0  27583  qqhval2lem  27584  eulerpartlemsv2  27923  eulerpartlemv  27929  eulerpartlemf  27935  eulerpartlemgh  27943  3orel1  28548  3orel13  28555  dfon2lem4  28781  dfon2lem6  28783  dfrdg4  29163  rankeq1o  29391  pellfund14gap  30414  wepwsolem  30580  fmul01lt1lem1  31089  cncfiooicclem1  31187
  Copyright terms: Public domain W3C validator