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  1701  hbimd  1723  hbim  1727  nfimd  1763  a16gALT  1887  sbi2  2003  ax46to6  2105  ax467to6  2112  ax467to7  2113  ax11indi  2136  mo  2166  mo2  2173  exmo  2189  2mo  2222  nrexrmo  2758  elab3gf  2920  moeq3  2943  opthpr  3791  dfopif  3794  dvdemo1  4209  reusv6OLD  4544  dfwe2  4572  ordunisuc2  4634  weniso  5814  xrub  10626  acsfn  13557  xkopt  17345  hbimtg  23567  meran1  24260  imsym1  24267  ordcmp  24296  wl-jarli  24312  wl-pm5.74  24328  lineval5a  25499  lppotoslem  25554  pm10.53  26972  pm11.63  27005  ax4567  27012  ax4567to4  27013  ax4567to6  27015  ax4567to7  27016  fnchoice  27111  conimpf  27277  3ornot23  27553  notnot2ALT  27575  hbimpg  27603  hbimpgVD  27960  notnot2ALTVD  27971  notnot2ALT2  27983  ax9lem9  28427  ax9lem10  28428
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator