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 21 . 2  |-  ( -. 
ph  ->  -.  ph )
21pm2.21d 100 1  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 5    -> wi 6
This theorem is referenced by:  pm2.24  103  pm2.18  104  notnot2  106  simplim  145  jarl  157  orel2  374  pm2.42  560  pm4.82  899  pm5.71  907  dedlem0b  924  dedlemb  926  dfnot  1328  cad0  1396  meredith  1400  tbw-bijust  1458  tbw-negdf  1459  ax12o10lem7  1641  ax12o10lem11  1645  a16gALT  1679  hbim  1723  nfimd  1727  ax46to6  1748  ax467to6  1754  ax467to7  1755  hbimd  1809  sbi2  1957  ax11indi  2112  mo  2138  mo2  2145  exmo  2161  2mo  2194  elab3gf  2870  moeq3  2893  opthpr  3731  dfopif  3734  dvdemo1  4148  reusv6OLD  4482  dfwe2  4510  ordunisuc2  4572  weniso  5751  xrub  10561  acsfn  13488  xkopt  17276  hbimtg  23497  meran1  24190  imsym1  24197  ordcmp  24226  wl-jarli  24242  wl-pm5.74  24258  lineval5a  25420  lppotoslem  25475  pm10.53  26893  pm11.63  26926  ax4567  26933  ax4567to4  26934  ax4567to6  26936  ax4567to7  26937  fnchoice  27033  conimpf  27140  3ornot23  27286  notnot2ALT  27308  hbimpg  27336  hbimpgVD  27693  notnot2ALTVD  27704  notnot2ALT2  27716  ax12dgen2K  28158  ax12o10lem7K  28172  ax12o10lem7X  28173  ax12o10lem11K  28180  ax12o10lem11X  28181  a16gALTX  28228  ax9lem9  28278  ax9lem10  28279
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator