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  1956  ax11indi  2109  mo  2135  mo2  2142  exmo  2158  2mo  2191  elab3gf  2856  moeq3  2879  opthpr  3690  dfopif  3693  dvdemo1  4104  reusv6OLD  4436  dfwe2  4464  ordunisuc2  4526  weniso  5704  xrub  10508  acsfn  13405  xkopt  17181  hbimtg  23331  meran1  24024  imsym1  24031  ordcmp  24060  wl-jarli  24076  wl-pm5.74  24092  lineval5a  25254  lppotoslem  25309  pm10.53  26727  pm11.63  26760  ax4567  26767  ax4567to4  26768  ax4567to6  26770  ax4567to7  26771  3ornot23  26963  notnot2ALT  26985  hbimpg  27013  hbimpgVD  27370  notnot2ALTVD  27381  notnot2ALT2  27393  ax9lem9  27837  ax9lem10  27838
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator