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

Theorem pm2.21 102
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 20 . 2  |-  ( -. 
ph  ->  -.  ph )
21pm2.21d 100 1  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.24  103  pm2.18  104  notnot2  106  simplim  145  jarl  157  orel2  373  pm2.42  558  pm4.82  895  pm5.71  903  dedlem0b  920  dedlemb  922  dfnot  1338  cad0  1406  meredith  1410  tbw-bijust  1469  tbw-negdf  1470  ax12dgen2  1733  19.38  1802  nfimdOLD  1818  hbimdOLD  1825  hbimOLD  1827  a16gOLD  1993  sbi2  2097  ax46to6  2198  ax467to6  2205  ax467to7  2206  ax11indi  2230  mo  2260  mo2  2267  exmo  2283  2mo  2316  nrexrmo  2868  elab3gf  3030  moeq3  3054  opthpr  3918  dfopif  3923  dvdemo1  4340  reusv6OLD  4674  dfwe2  4702  ordunisuc2  4764  weniso  6014  0neqopab  6058  bropopvvv  6365  xrub  10822  injresinjlem  11126  hashnnn0genn0  11554  hashprb  11595  hash1snb  11608  hashgt12el  11609  hashgt12el2  11610  hash2prde  11615  acsfn  13811  xkopt  17608  wlkdvspthlem  21455  usgrcyclnl2  21476  constr3trllem2  21486  hbimtg  25187  meran1  25875  imsym1  25882  ordcmp  25911  wl-jarli  25927  wl-pm5.74  25942  pm10.53  27230  pm11.63  27263  ax4567  27270  ax4567to4  27271  ax4567to6  27273  ax4567to7  27274  frgra3vlem1  27753  2pthfrgra  27764  frgrancvvdeqlem2  27783  frgrawopreglem3  27798  frgraregorufr  27805  3ornot23  27934  notnot2ALT  27956  hbimpg  27984  hbimpgVD  28357  notnot2ALTVD  28368  a16gNEW7  28882  sbi2NEW7  28900
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator