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 113
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 138. (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 111 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  114  pm2.18  115  notnotr  118  simplim  158  jarl  170  orel2  392  pm2.42  590  pm4.82  955  pm5.71  963  dedlem0b  982  dedlemb  984  cases2  995  cad0  1544  meredith  1554  tbw-bijust  1611  tbw-negdf  1612  19.38  1743  19.35  1771  ax13dgen2  1962  sbi2  2276  mo2v  2360  exmo  2378  2mo  2434  axin2  2474  nrexrmo  3033  elab3gf  3214  moeq3  3239  opthpr  4182  dfopif  4193  dvdemo1  4676  weniso  6318  0neqopab  6409  dfwe2  6685  ordunisuc2  6748  0mnnnnn0  10993  nn0ge2m1nn  11025  xrub  11692  injresinjlem  12131  fleqceilz  12189  addmodlteq  12273  fsuppmapnn0fiub0  12319  hashnnn0genn0  12640  hashprb  12692  hash1snb  12714  hashgt12el  12716  hashgt12el2  12717  hash2prde  12754  hashge2el2dif  12760  hashge2el2difr  12761  lcmf  14768  prmgaplem5  15187  cshwshashlem1  15227  acsfn  15731  symgfix2  17218  0ringnnzr  18652  mndifsplit  19819  symgmatr01lem  19836  xkopt  20827  wlkdvspthlem  25498  usgrcyclnl2  25530  constr3trllem2  25540  clwlknclwlkdifs  25848  frgra3vlem1  25888  2pthfrgra  25899  frgrancvvdeqlem2  25919  frgrawopreglem3  25934  frgraregorufr  25941  frgraregord013  26006  hbimtg  30604  meran1  31220  imsym1  31227  ordcmp  31256  bj-curry  31321  bj-babygodel  31371  bj-ssbid2ALT  31441  bj-dvdemo1  31599  wl-jarli  32063  wl-lem-nexmo  32127  wl-ax11-lem2  32141  tsim2  32609  axc5c7toc7  32717  axc5c711toc7  32724  axc5c711to11  32725  ax12indi  32748  ifpim23g  36379  pm10.53  37072  pm11.63  37102  axc5c4c711  37109  axc5c4c711toc5  37110  axc5c4c711toc7  37112  axc5c4c711to11  37113  3ornot23  37221  notnotrALT  37242  hbimpg  37277  hbimpgVD  37649  notnotrALTVD  37660  nn0o1gt2ALTV  39343  nn0oALTV  39345  gboge7  39384  nnsum3primesle9  39409  bgoldbtbndlem1  39420  umgrislfupgrlem  39747  lfgrwlkprop  40296  clwwlknclwwlkdifs  40581  frgr3vlem1  40843  frgrncvvdeqlem2  40870  frgrwopreglem3  40883  frgrregorufr  40890  av-frgraregord013  40949  lindslinindsimp1  41440
  Copyright terms: Public domain W3C validator