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

Theorem orel2 383
Description: Elimination of disjunction by denial of a disjunct. Theorem *2.56 of [WhiteheadRussell] p. 107. (Contributed by NM, 12-Aug-1994.) (Proof shortened by Wolf Lammen, 5-Apr-2013.)
Assertion
Ref Expression
orel2  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )

Proof of Theorem orel2
StepHypRef Expression
1 idd 24 . 2  |-  ( -. 
ph  ->  ( ps  ->  ps ) )
2 pm2.21 108 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2jaod 380 1  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  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:  biorfi  407  pm2.64  787  pm2.74  844  pm5.71  934  prel12  4188  xpcan2  5430  funun  5616  ablfac1eulem  16991  drngmuleq0  17287  mdetunilem9  18989  maducoeval2  19009  tdeglem4  22324  deg1sublt  22377  dvply1  22545  aaliou2  22601  colline  23895  axcontlem2  24133  3orel3  28955  dfrdg4  29568  arg-ax  29849  elpell14qr2  30766  elpell1qr2  30776  jm2.22  30905  jm2.23  30906  jm2.26lem3  30911  ttac  30946  wepwsolem  30955  dgrnznn  31053  fmul01lt1lem2  31503  cncfiooicclem1  31599  3ornot23VD  33355
  Copyright terms: Public domain W3C validator