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

Theorem pm2.21 100
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 19 . 2  |-  ( -. 
ph  ->  -.  ph )
21pm2.21d 98 1  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.24  101  pm2.18  102  notnot2  104  simplim  143  jarl  155  orel2  372  pm2.42  557  pm4.82  894  pm5.71  902  dedlem0b  919  dedlemb  921  dfnot  1322  cad0  1390  meredith  1394  tbw-bijust  1453  tbw-negdf  1454  ax12dgen2  1702  hbimd  1723  hbim  1727  nfimd  1763  a16g  1887  sbi2  2006  ax46to6  2105  ax467to6  2112  ax467to7  2113  ax11indi  2137  mo  2167  mo2  2174  exmo  2190  2mo  2223  nrexrmo  2759  elab3gf  2921  moeq3  2944  opthpr  3792  dfopif  3795  dvdemo1  4212  reusv6OLD  4547  dfwe2  4575  ordunisuc2  4637  weniso  5854  xrub  10632  acsfn  13563  xkopt  17351  hbimtg  24165  meran1  24852  imsym1  24859  ordcmp  24888  wl-jarli  24904  wl-pm5.74  24920  lineval5a  26099  lppotoslem  26154  pm10.53  27572  pm11.63  27605  ax4567  27612  ax4567to4  27613  ax4567to6  27615  ax4567to7  27616  fnchoice  27711  conimpf  27897  frgra3vlem1  28189  3ornot23  28326  notnot2ALT  28348  hbimpg  28376  hbimpgVD  28753  notnot2ALTVD  28764  notnot2ALT2  28776  ax9lem9  29221  ax9lem10  29222
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator