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

Theorem pm2.21 103
Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Sep-2012.)
Assertion
Ref Expression
pm2.21  |-  ( -. 
ph  ->  ( ph  ->  ps ) )

Proof of Theorem pm2.21
StepHypRef Expression
1 id 21 . 2  |-  ( -. 
ph  ->  -.  ph )
21pm2.21d 101 1  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.24  104  pm2.18  105  notnot2  107  simplim  146  jarl  158  orel2  374  pm2.42  559  pm4.82  896  pm5.71  904  dedlem0b  921  dedlemb  923  dfnot  1342  cad0  1410  meredith  1414  tbw-bijust  1473  tbw-negdf  1474  ax12dgen2  1742  19.38  1813  nfimdOLD  1829  hbimdOLD  1836  hbimOLD  1838  a16gOLD  2050  sbi2  2135  ax46to6  2243  ax467to6  2250  ax467to7  2251  ax11indi  2275  mo  2305  mo2  2312  exmo  2328  2mo  2361  axin2  2408  nrexrmo  2927  elab3gf  3089  moeq3  3113  opthpr  3978  dfopif  3983  dvdemo1  4402  reusv6OLD  4737  dfwe2  4765  ordunisuc2  4827  weniso  6078  0neqopab  6122  bropopvvv  6429  xrub  10895  injresinjlem  11204  hashnnn0genn0  11632  hashprb  11673  hash1snb  11686  hashgt12el  11687  hashgt12el2  11688  hash2prde  11693  acsfn  13889  xkopt  17692  wlkdvspthlem  21612  usgrcyclnl2  21633  constr3trllem2  21643  hbimtg  25439  meran1  26166  imsym1  26173  ordcmp  26202  wl-jarli  26218  wl-pm5.74  26233  wl-sbrim  26242  pm10.53  27552  pm11.63  27585  ax4567  27592  ax4567to4  27593  ax4567to6  27595  ax4567to7  27596  0mnnnnn0  28118  euhash1  28190  swrdvalodm2  28222  cshwssizelem1a  28313  cshwssizelem3  28316  frgra3vlem1  28464  2pthfrgra  28475  frgrancvvdeqlem2  28494  frgrawopreglem3  28509  frgraregorufr  28516  3ornot23  28665  notnot2ALT  28687  hbimpg  28715  hbimpgVD  29090  notnot2ALTVD  29101  a16gNEW7  29620  sbi2NEW7  29638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator