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

Theorem pm2.21 118
Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. Its associated inference is pm2.21i 114. (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 116 1 𝜑 → (𝜑𝜓))
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  119  pm2.18  120  notnotr  123  simplim  161  jarl  173  orel2  396  pm2.42  595  pm4.82  964  pm5.71  972  dedlem0b  991  dedlemb  993  cases2  1004  cad0  1546  meredith  1556  tbw-bijust  1613  tbw-negdf  1614  19.38  1745  19.35  1775  ax13dgen2  1963  sbi2  2285  mo2v  2369  exmo  2387  2mo  2443  axin2  2483  nrexrmo  3044  elab3gf  3229  moeq3  3254  opthpr  4223  dfopif  4235  dvdemo1  4728  weniso  6380  0neqopab  6472  dfwe2  6748  ordunisuc2  6811  0mnnnnn0  11079  nn0ge2m1nn  11114  xrub  11879  injresinjlem  12317  fleqceilz  12382  addmodlteq  12474  fsuppmapnn0fiub0  12522  hashnnn0genn0  12857  hashprb  12909  hash1snb  12931  hashgt12el  12933  hashgt12el2  12934  hash2prde  12972  hashge2el2dif  12978  hashge2el2difr  12979  dvdsaddre2b  14734  lcmf  15058  prmgaplem5  15479  cshwshashlem1  15522  acsfn  16033  symgfix2  17549  0ringnnzr  18992  mndifsplit  20162  symgmatr01lem  20179  xkopt  21169  wlkdvspthlem  25876  usgrcyclnl2  25908  constr3trllem2  25918  clwlknclwlkdifs  26226  frgra3vlem1  26266  2pthfrgra  26277  frgrancvvdeqlem2  26297  frgrawopreglem3  26312  frgraregorufr  26319  frgraregord013  26384  hbimtg  30799  meran1  31415  imsym1  31422  ordcmp  31451  bj-curry  31547  bj-babygodel  31596  bj-ssbid2ALT  31670  bj-dvdemo1  31832  wl-nfimd  32314  wl-nfim1  32332  wl-jarli  32342  wl-lem-nexmo  32403  wl-ax11-lem2  32417  tsim2  32983  axc5c7toc7  33091  axc5c711toc7  33098  axc5c711to11  33099  ax12indi  33122  ifpim23g  36741  clsk1indlem3  37243  pm10.53  37469  pm11.63  37499  axc5c4c711  37506  axc5c4c711toc5  37507  axc5c4c711toc7  37509  axc5c4c711to11  37510  3ornot23  37618  notnotrALT  37638  hbimpg  37673  hbimpgVD  38044  notnotrALTVD  38055  prminf2  39933  nn0o1gt2ALTV  40038  nn0oALTV  40040  gboge7  40080  nnsum3primesle9  40105  bgoldbtbndlem1  40116  umgrislfupgrlem  40439  lfgrwlkprop  40988  clwwlknclwwlkdifs  41273  frgr3vlem1  41535  frgrncvvdeqlem2  41562  frgrwopreglem3  41575  frgrregorufr  41582  av-frgraregord013  41641  lindslinindsimp1  42132
  Copyright terms: Public domain W3C validator