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  2113  mo  2140  mo2  2147  exmo  2163  2mo  2196  nrexrmo  2732  elab3gf  2894  moeq3  2917  opthpr  3764  dfopif  3767  dvdemo1  4182  reusv6OLD  4517  dfwe2  4545  ordunisuc2  4607  weniso  5786  xrub  10597  acsfn  13524  xkopt  17312  hbimtg  23533  meran1  24226  imsym1  24233  ordcmp  24262  wl-jarli  24278  wl-pm5.74  24294  lineval5a  25456  lppotoslem  25511  pm10.53  26929  pm11.63  26962  ax4567  26969  ax4567to4  26970  ax4567to6  26972  ax4567to7  26973  fnchoice  27069  conimpf  27235  3ornot23  27406  notnot2ALT  27428  hbimpg  27456  hbimpgVD  27813  notnot2ALTVD  27824  notnot2ALT2  27836  ax12dgen2K  28278  ax12o10lem7K  28292  ax12o10lem7X  28293  ax12o10lem11K  28300  ax12o10lem11X  28301  a16gALTX  28348  ax9lem9  28398  ax9lem10  28399
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10
  Copyright terms: Public domain W3C validator