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

Theorem orel2 372
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 21 . 2  |-  ( -. 
ph  ->  ( ps  ->  ps ) )
2 pm2.21 100 . 2  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
31, 2jaod 369 1  |-  ( -. 
ph  ->  ( ( ps  \/  ph )  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    \/ wo 357
This theorem is referenced by:  biorfi  396  pm2.64  764  pm2.74  819  pm5.71  902  prel12  3789  xpcan2  5113  funun  5296  ablfac1eulem  15307  drngmuleq0  15535  tdeglem4  19446  deg1sublt  19496  dvply1  19664  aaliou2  19720  3orel3  24063  dfrdg4  24488  axcontlem2  24593  arg-ax  24855  elpell14qr2  26947  elpell1qr2  26957  jm2.22  27088  jm2.23  27089  jm2.26lem3  27094  ttac  27129  wepwsolem  27138  dgrnznn  27340  fmul01lt1lem2  27715  3ornot23VD  28623
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
  Copyright terms: Public domain W3C validator