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  1700  hbimd  1721  hbim  1725  nfimd  1761  a16g  1885  sbi2  2004  ax46to6  2103  ax467to6  2110  ax467to7  2111  ax11indi  2135  mo  2165  mo2  2172  exmo  2188  2mo  2221  nrexrmo  2757  elab3gf  2919  moeq3  2942  opthpr  3790  dfopif  3793  dvdemo1  4210  reusv6OLD  4545  dfwe2  4573  ordunisuc2  4635  weniso  5852  xrub  10630  acsfn  13561  xkopt  17349  hbimtg  24163  meran1  24850  imsym1  24857  ordcmp  24886  wl-jarli  24902  wl-pm5.74  24918  lineval5a  26088  lppotoslem  26143  pm10.53  27561  pm11.63  27594  ax4567  27601  ax4567to4  27602  ax4567to6  27604  ax4567to7  27605  fnchoice  27700  conimpf  27886  frgra3vlem1  28178  3ornot23  28270  notnot2ALT  28292  hbimpg  28320  hbimpgVD  28680  notnot2ALTVD  28691  notnot2ALT2  28703  ax9lem9  29148  ax9lem10  29149
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator