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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	pm2.21d 121	1 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))

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  1878  ax13dgen2  2139  ax13dgen4  2141  nfim1  2197  sbi2  2306  sbi2ALT  2583  dfmoeu  2594  nexmo  2599  2mo  2710  axin2  2759  r19.35  3295  nrexrmo  3380  elab3gf  3620  moeq3  3651  opthpr  4742  preqsnd  4749  opthprneg  4755  dfopif  4760  dvdemo1  5239  axprlem1  5289  axprlem5  5293  snopeqop  5361  0nelopab  5417  weniso  7086  dfwe2  7476  ordunisuc2  7539  0mnnnnn0  11917  nn0ge2m1nn  11952  xrub  12693  injresinjlem  13152  fleqceilz  13217  addmodlteq  13309  fsuppmapnn0fiub0  13356  expnngt1  13598  hashnnn0genn0  13699  hashprb  13754  hash1snb  13776  hashgt12el  13779  hashgt12el2  13780  hash2prde  13824  hashge2el2dif  13834  hashge2el2difr  13835  dvdsaddre2b  15649  lcmf  15967  prmgaplem5  16381  cshwshashlem1  16421  acsfn  16922  symgfix2  18536  0ringnnzr  20035  mndifsplit  21241  symgmatr01lem  21258  xkopt  22260  umgrislfupgrlem  26915  lfgrwlkprop  27477  frgr3vlem1  28058  frgrwopreg  28108  frgrregorufr  28110  frgrregord013  28180  9p10ne21fool  28256  satffunlem1lem1  32762  satffunlem2lem1  32764  jath  33071  hbimtg  33164  meran1  33872  imsym1  33879  ordcmp  33908  bj-babygodel  34050  bj-ssbid2ALT  34109  wl-lem-nexmo  34968  wl-ax11-lem2  34983  nexmo1  35668  axc5c7toc7  36209  axc5c711toc7  36216  axc5c711to11  36217  ax12indi  36240  sbn1  39394  ifpim23g  40203  clsk1indlem3  40746  pm10.53  41070  pm11.63  41099  axc5c4c711  41105  axc5c4c711toc5  41106  axc5c4c711toc7  41108  axc5c4c711to11  41109  3ornot23  41215  notnotrALT  41235  hbimpg  41260  hbimpgVD  41610  notnotrALTVD  41621  climxrre  42392  liminf0  42435  prprelprb  44034  prminf2  44105  nn0o1gt2ALTV  44212  nn0oALTV  44214  gbowge7  44281  nnsum3primesle9  44312  bgoldbtbndlem1  44323  lindslinindsimp1  44866