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  1756  19.35  1793  nfimd  1811  ax13dgen2  2001  ax13dgen4  2003  nfim1  2053  sbi2  2380  mo2v  2464  exmo  2482  2mo  2538  axin2  2578  nrexrmo  3139  elab3gf  3324  moeq3  3349  opthpr  4319  dfopif  4331  dvdemo1  4824  weniso  6482  0neqopab  6574  dfwe2  6850  ordunisuc2  6913  0mnnnnn0  11172  nn0ge2m1nn  11207  xrub  11970  injresinjlem  12405  fleqceilz  12470  addmodlteq  12562  fsuppmapnn0fiub0  12610  hashnnn0genn0  12945  hashprb  12998  hash1snb  13020  hashgt12el  13022  hashgt12el2  13023  hash2prde  13061  hashge2el2dif  13067  hashge2el2difr  13068  dvdsaddre2b  14813  lcmf  15130  prmgaplem5  15543  cshwshashlem1  15586  acsfn  16089  symgfix2  17605  0ringnnzr  19036  mndifsplit  20203  symgmatr01lem  20220  xkopt  21210  wlkdvspthlem  25903  usgrcyclnl2  25935  constr3trllem2  25945  clwlknclwlkdifs  26253  frgra3vlem1  26293  2pthfrgra  26304  frgrancvvdeqlem2  26324  frgrawopreglem3  26339  frgraregorufr  26346  frgraregord013  26411  hbimtg  30762  meran1  31386  imsym1  31393  ordcmp  31422  bj-curry  31518  bj-babygodel  31567  bj-ssbid2ALT  31641  bj-dvdemo1  31803  wl-jarli  32271  wl-lem-nexmo  32331  wl-ax11-lem2  32345  tsim2  32911  axc5c7toc7  33019  axc5c711toc7  33026  axc5c711to11  33027  ax12indi  33050  ifpim23g  36662  clsk1indlem3  37164  pm10.53  37390  pm11.63  37420  axc5c4c711  37427  axc5c4c711toc5  37428  axc5c4c711toc7  37430  axc5c4c711to11  37431  3ornot23  37539  notnotrALT  37559  hbimpg  37594  hbimpgVD  37965  notnotrALTVD  37976  prminf2  39843  nn0o1gt2ALTV  39948  nn0oALTV  39950  gboge7  39990  nnsum3primesle9  40015  bgoldbtbndlem1  40026  umgrislfupgrlem  40349  lfgrwlkprop  40898  clwwlknclwwlkdifs  41183  frgr3vlem1  41445  frgrncvvdeqlem2  41472  frgrwopreglem3  41485  frgrregorufr  41492  av-frgraregord013  41551  lindslinindsimp1  42042
  Copyright terms: Public domain W3C validator