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 120
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 116. (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 118 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  121  pm2.18  122  notnotr  125  simplim  163  jarl  175  orel2  397  pm2.42  597  pm4.82  989  pm5.71  997  dedlem0b  1013  dedlemb  1015  cases2ALT  1017  cad0  1596  meredith  1606  tbw-bijust  1663  tbw-negdf  1664  19.38  1806  19.35  1845  nfimdOLDOLD  1864  ax13dgen2  2055  ax13dgen4  2057  nfim1  2105  sbi2  2421  mo2v  2505  exmo  2523  2mo  2580  axin2  2620  nrexrmo  3193  elab3gf  3388  moeq3  3416  opthpr  4415  dfopif  4430  dvdemo1  4932  weniso  6644  0neqopab  6740  dfwe2  7023  ordunisuc2  7086  0mnnnnn0  11363  nn0ge2m1nn  11398  xrub  12180  injresinjlem  12628  fleqceilz  12693  addmodlteq  12785  fsuppmapnn0fiub0  12833  hashnnn0genn0  13171  hashprb  13223  hash1snb  13245  hashgt12el  13248  hashgt12el2  13249  hash2prde  13290  hashge2el2dif  13300  hashge2el2difr  13301  dvdsaddre2b  15076  lcmf  15393  prmgaplem5  15806  cshwshashlem1  15849  acsfn  16367  symgfix2  17882  0ringnnzr  19317  mndifsplit  20490  symgmatr01lem  20507  xkopt  21506  umgrislfupgrlem  26062  lfgrwlkprop  26640  clwwlknclwwlkdifsOLD  26947  frgr3vlem1  27253  frgrwopreg  27303  frgrregorufr  27305  frgrregord013  27382  jath  31735  hbimtg  31836  meran1  32535  imsym1  32542  ordcmp  32571  bj-curry  32667  bj-babygodel  32713  bj-ssbid2ALT  32771  bj-dvdemo1  32927  wl-jarli  33419  wl-lem-nexmo  33479  wl-ax11-lem2  33493  tsim2  34068  nexmo  34153  axc5c7toc7  34517  axc5c711toc7  34524  axc5c711to11  34525  ax12indi  34548  ifpim23g  38157  clsk1indlem3  38658  pm10.53  38882  pm11.63  38912  axc5c4c711  38919  axc5c4c711toc5  38920  axc5c4c711toc7  38922  axc5c4c711to11  38923  3ornot23  39032  notnotrALT  39052  hbimpg  39087  hbimpgVD  39454  notnotrALTVD  39465  climxrre  40300  liminf0  40343  prminf2  41825  nn0o1gt2ALTV  41930  nn0oALTV  41932  gbowge7  41976  nnsum3primesle9  42007  bgoldbtbndlem1  42018  lindslinindsimp1  42571
  Copyright terms: Public domain W3C validator