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

Theorem pm2.21 108
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, 29-Dec-1992.) (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 22 . 2  |-  ( -. 
ph  ->  -.  ph )
21pm2.21d 106 1  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm2.24  109  pm2.18  110  notnot2  112  simplim  151  jarl  163  orel2  383  pm2.42  574  pm4.82  926  pm5.71  934  dedlem0b  951  dedlemb  953  cases2  970  cases2OLD  971  dfnotOLD  1399  cad0  1452  meredith  1456  tbw-bijust  1515  tbw-negdf  1516  19.38  1639  19.35  1664  ax13dgen2  1783  sbi2  2108  axc5c7toc7  2236  axc5c711toc7  2243  axc5c711to11  2244  ax12indi  2267  mo2v  2282  mo2vOLD  2283  mo2vOLDOLD  2284  exmo  2304  moOLD  2327  mo2OLD  2336  2mo  2382  2moOLD  2383  2moOLDOLD  2384  axin2  2434  nrexrmo  3081  elab3gf  3255  moeq3  3280  opthpr  4204  dfopif  4210  reusv6OLD  4658  dvdemo1  4682  weniso  6239  0neqopab  6326  dfwe2  6602  ordunisuc2  6664  bropopvvv  6864  0mnnnnn0  10829  nn0ge2m1nn  10862  xrub  11504  injresinjlem  11894  fleqceilz  11950  fsuppmapnn0fiub0  12068  hashnnn0genn0  12385  hashprb  12431  hash1snb  12445  euhash1  12446  hashgt12el  12447  hashgt12el2  12448  hash2prde  12483  hashge2el2dif  12488  swrdvalodm2  12630  cshwshashlem1  14441  acsfn  14917  symgfix2  16255  0rngnnzr  17728  mndifsplit  18945  symgmatr01lem  18962  xkopt  19983  wlkdvspthlem  24382  usgrcyclnl2  24414  constr3trllem2  24424  clwlknclwlkdifs  24733  frgra3vlem1  24773  2pthfrgra  24784  frgrancvvdeqlem2  24805  frgrawopreglem3  24820  frgraregorufr  24827  frgraregord013  24892  hbimtg  29092  meran1  29729  imsym1  29736  ordcmp  29765  wl-jarli  29823  wl-lem-nexmo  29869  wl-ax11-lem2  29879  tsim2  30369  pm10.53  31076  pm11.63  31106  axc5c4c711  31113  axc5c4c711toc5  31114  axc5c4c711toc7  31116  axc5c4c711to11  31117  lindslinindsimp1  32356  3ornot23  32574  notnot2ALT  32595  hbimpg  32624  hbimpgVD  33001  notnot2ALTVD  33012  bj-iffal  33451  bj-babygodel  33490  bj-dvdemo1  33686
  Copyright terms: Public domain W3C validator