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 123
Description: From a wff and its negation, anything follows. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. Its commuted form is pm2.24 124 and its associated inference is pm2.21i 119. (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 121 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  124  jarl  125  jarli  126  pm2.18d  127  pm2.18OLD  129  simplim  168  orel2  884  curryax  887  pm2.42  936  pm4.82  1017  pm5.71  1021  dedlem0b  1036  dedlemb  1038  cases2ALT  1040  cad0  1609  meredith  1633  tbw-bijust  1690  tbw-negdf  1691  nfntht  1785  19.38  1830  19.35  1869  ax13dgen2  2133  ax13dgen4  2135  nfim1  2189  sbi2  2301  sbi2vOLD  2315  sbi2ALT  2600  dfmoeu  2611  nexmo  2616  2mo  2726  axin2  2777  r19.35  3338  nrexrmo  3433  elab3gf  3669  moeq3  3700  opthpr  4774  preqsnd  4781  opthprneg  4787  dfopif  4792  dvdemo1  5265  axprlem1  5314  axprlem5  5318  snopeqop  5387  0nelopab  5443  weniso  7096  dfwe2  7485  ordunisuc2  7548  0mnnnnn0  11917  nn0ge2m1nn  11952  xrub  12693  injresinjlem  13145  fleqceilz  13210  addmodlteq  13302  fsuppmapnn0fiub0  13349  expnngt1  13590  hashnnn0genn0  13691  hashprb  13746  hash1snb  13768  hashgt12el  13771  hashgt12el2  13772  hash2prde  13816  hashge2el2dif  13826  hashge2el2difr  13827  dvdsaddre2b  15645  lcmf  15965  prmgaplem5  16379  cshwshashlem1  16417  acsfn  16918  symgfix2  18473  0ringnnzr  19970  mndifsplit  21173  symgmatr01lem  21190  xkopt  22191  umgrislfupgrlem  26834  lfgrwlkprop  27396  frgr3vlem1  27979  frgrwopreg  28029  frgrregorufr  28031  frgrregord013  28101  9p10ne21fool  28177  satffunlem1lem1  32546  satffunlem2lem1  32548  jath  32855  hbimtg  32948  meran1  33656  imsym1  33663  ordcmp  33692  bj-babygodel  33834  bj-ssbid2ALT  33893  wl-lem-nexmo  34684  wl-ax11-lem2  34699  nexmo1  35389  axc5c7toc7  35929  axc5c711toc7  35936  axc5c711to11  35937  ax12indi  35960  sbn1  38981  ifpim23g  39739  clsk1indlem3  40271  pm10.53  40575  pm11.63  40604  axc5c4c711  40610  axc5c4c711toc5  40611  axc5c4c711toc7  40613  axc5c4c711to11  40614  3ornot23  40720  notnotrALT  40740  hbimpg  40765  hbimpgVD  41115  notnotrALTVD  41126  climxrre  41907  liminf0  41950  prprelprb  43556  prminf2  43627  nn0o1gt2ALTV  43736  nn0oALTV  43738  gbowge7  43805  nnsum3primesle9  43836  bgoldbtbndlem1  43847  lindslinindsimp1  44440
  Copyright terms: Public domain W3C validator