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  919  pm5.71  927  dedlem0b  944  dedlemb  946  cases2  963  dfnotOLD  1389  cad0  1442  meredith  1446  tbw-bijust  1505  tbw-negdf  1506  19.38  1629  19.35  1654  ax13dgen2  1772  sbi2  2085  axc5c7toc7  2214  axc5c711toc7  2221  axc5c711to11  2222  ax12indi  2245  mo2v  2260  mo2vOLD  2261  mo2vOLDOLD  2262  exmo  2282  moOLD  2305  mo2OLD  2314  2mo  2360  2moOLD  2361  2moOLDOLD  2362  axin2  2412  nrexrmo  2961  elab3gf  3132  moeq3  3157  opthpr  4071  dfopif  4077  reusv6OLD  4524  dvdemo1  4548  weniso  6066  0neqopab  6152  dfwe2  6414  ordunisuc2  6476  bropopvvv  6674  0mnnnnn0  10633  xrub  11295  injresinjlem  11659  fleqceilz  11714  hashnnn0genn0  12135  hashprb  12178  hash1snb  12192  euhash1  12193  hashgt12el  12194  hashgt12el2  12195  hash2prde  12200  hashge2el2dif  12205  swrdvalodm2  12354  cshwshashlem1  14143  acsfn  14618  symgfix2  15942  mndifsplit  18464  symgmatr01lem  18481  xkopt  19250  wlkdvspthlem  23528  usgrcyclnl2  23549  constr3trllem2  23559  hbimtg  27642  meran1  28279  imsym1  28286  ordcmp  28315  wl-jarli  28373  wl-lem-nexmo  28418  wl-ax11-lem2  28428  tsim2  28968  pm10.53  29644  pm11.63  29674  axc5c4c711  29681  axc5c4c711toc5  29682  axc5c4c711toc7  29684  axc5c4c711to11  29685  clwlknclwlkdifs  30604  frgra3vlem1  30618  2pthfrgra  30629  frgrancvvdeqlem2  30650  frgrawopreglem3  30665  frgraregorufr  30672  frgraregord013  30737  0rngnnzr  30808  fsuppmapnn0fiub0  30831  lindslinindsimp1  30988  3ornot23  31309  notnot2ALT  31330  hbimpg  31359  hbimpgVD  31736  notnot2ALTVD  31747  bj-iffal  32186  bj-babygodel  32219  bj-dvdemo1  32419
  Copyright terms: Public domain W3C validator