MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21 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

Proof of Theorem pm2.21
StepHypRef Expression
1 id 22 . 2
21pm2.21d 106 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4
This theorem is referenced by:  pm2.24  109  pm2.18  110  notnot2  112  simplim  151  jarl  163  orel2  383  pm2.42  574  pm4.82  928  pm5.71  936  dedlem0b  953  dedlemb  955  cases2  971  ifpfal  1389  dfnotOLD  1415  cad0  1467  meredith  1472  tbw-bijust  1531  tbw-negdf  1532  19.38  1662  19.35  1687  ax13dgen2  1834  sbi2  2134  axc5c7toc7  2243  axc5c711toc7  2250  axc5c711to11  2251  ax12indi  2274  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  exmo  2309  mo2OLD  2334  2mo  2373  2moOLD  2374  axin2  2424  nrexrmo  3077  elab3gf  3251  moeq3  3276  opthpr  4208  dfopif  4214  reusv6OLD  4663  dvdemo1  4687  weniso  6250  0neqopab  6341  dfwe2  6617  ordunisuc2  6679  0mnnnnn0  10853  nn0ge2m1nn  10886  xrub  11532  injresinjlem  11925  fleqceilz  11981  fsuppmapnn0fiub0  12099  hashnnn0genn0  12416  hashprb  12462  hash1snb  12479  hashgt12el  12481  hashgt12el2  12482  hash2prde  12516  hashge2el2dif  12521  swrdvalodm2  12664  cshwshashlem1  14580  acsfn  15056  symgfix2  16441  0ringnnzr  17917  mndifsplit  19138  symgmatr01lem  19155  xkopt  20156  wlkdvspthlem  24609  usgrcyclnl2  24641  constr3trllem2  24651  clwlknclwlkdifs  24960  frgra3vlem1  25000  2pthfrgra  25011  frgrancvvdeqlem2  25031  frgrawopreglem3  25046  frgraregorufr  25053  frgraregord013  25118  hbimtg  29239  meran1  29876  imsym1  29883  ordcmp  29912  wl-jarli  29970  wl-lem-nexmo  30016  wl-ax11-lem2  30026  tsim2  30538  pm10.53  31271  pm11.63  31301  axc5c4c711  31308  axc5c4c711toc5  31309  axc5c4c711toc7  31311  axc5c4c711to11  31312  lindslinindsimp1  33058  3ornot23  33278  notnot2ALT  33299  hbimpg  33327  hbimpgVD  33704  notnot2ALTVD  33715  bj-babygodel  34191  bj-dvdemo1  34388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
  Copyright terms: Public domain W3C validator