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  170  orel2  888  curryax  891  pm2.42  940  pm4.82  1021  pm5.71  1025  dedlem0b  1040  dedlemb  1042  cases2ALT  1044  cad0  1619  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  nfntht  1795  19.38  1840  19.35  1879  ax13dgen2  2143  ax13dgen4  2145  nfim1  2201  sbi2  2312  sbi2vOLD  2326  sbi2ALT  2609  dfmoeu  2620  nexmo  2625  2mo  2736  axin2  2785  r19.35  3332  nrexrmo  3418  elab3gf  3658  moeq3  3689  opthpr  4766  preqsnd  4773  opthprneg  4779  dfopif  4784  dvdemo1  5261  axprlem1  5311  axprlem5  5315  snopeqop  5383  0nelopab  5439  weniso  7100  dfwe2  7490  ordunisuc2  7553  0mnnnnn0  11926  nn0ge2m1nn  11961  xrub  12702  injresinjlem  13161  fleqceilz  13226  addmodlteq  13318  fsuppmapnn0fiub0  13365  expnngt1  13607  hashnnn0genn0  13708  hashprb  13763  hash1snb  13785  hashgt12el  13788  hashgt12el2  13789  hash2prde  13833  hashge2el2dif  13843  hashge2el2difr  13844  dvdsaddre2b  15657  lcmf  15975  prmgaplem5  16389  cshwshashlem1  16429  acsfn  16930  symgfix2  18544  0ringnnzr  20042  mndifsplit  21245  symgmatr01lem  21262  xkopt  22263  umgrislfupgrlem  26918  lfgrwlkprop  27480  frgr3vlem1  28061  frgrwopreg  28111  frgrregorufr  28113  frgrregord013  28183  9p10ne21fool  28259  satffunlem1lem1  32706  satffunlem2lem1  32708  jath  33015  hbimtg  33108  meran1  33816  imsym1  33823  ordcmp  33852  bj-babygodel  33994  bj-ssbid2ALT  34053  wl-lem-nexmo  34913  wl-ax11-lem2  34928  nexmo1  35613  axc5c7toc7  36154  axc5c711toc7  36161  axc5c711to11  36162  ax12indi  36185  sbn1  39330  ifpim23g  40119  clsk1indlem3  40665  pm10.53  40990  pm11.63  41019  axc5c4c711  41025  axc5c4c711toc5  41026  axc5c4c711toc7  41028  axc5c4c711to11  41029  3ornot23  41135  notnotrALT  41155  hbimpg  41180  hbimpgVD  41530  notnotrALTVD  41541  climxrre  42318  liminf0  42361  prprelprb  43960  prminf2  44031  nn0o1gt2ALTV  44138  nn0oALTV  44140  gbowge7  44207  nnsum3primesle9  44238  bgoldbtbndlem1  44249  lindslinindsimp1  44792
 Copyright terms: Public domain W3C validator