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  simplim  167  orel2  888  curryax  891  pm2.42  940  pm4.82  1021  pm5.71  1025  dedlem0b  1042  dedlemb  1044  cases2ALT  1046  cad0  1611  cad0OLD  1612  meredith  1635  tbw-bijust  1692  tbw-negdf  1693  nfntht  1787  19.38  1833  19.35  1872  sbn1  2097  ax13dgen2  2126  ax13dgen4  2128  nfim1  2187  sbi2  2291  dfmoeu  2524  nexmo  2529  2mo  2636  axin2  2685  r19.35  3097  r19.35OLD  3098  r19.21v  3169  nrexrmo  3384  elab3gf  3670  elab3g  3671  moeq3  3704  dfss2  3962  ralidmw  4509  rzal  4510  ralidm  4513  opthpr  4854  opthprneg  4867  dfopif  4872  dvdemo1  5373  axprlem1  5423  axprlem5  5427  snopeqop  5508  0nelopabOLD  5570  weniso  7361  dfwe2  7777  ordunisuc2  7849  0mnnnnn0  12542  nn0ge2m1nn  12579  xrub  13331  injresinjlem  13793  fleqceilz  13860  addmodlteq  13952  fsuppmapnn0fiub0  13999  expnngt1  14244  hashnnn0genn0  14343  hashprb  14397  hash1snb  14419  hashgt12el  14422  hashgt12el2  14423  hash2prde  14472  hashge2el2dif  14482  hashge2el2difr  14483  dvdsaddre2b  16292  lcmf  16612  prmgaplem5  17032  cshwshashlem1  17073  acsfn  17647  symgfix2  19388  0ringnnzr  20479  mndifsplit  22587  symgmatr01lem  22604  xkopt  23608  umgrislfupgrlem  29012  lfgrwlkprop  29578  frgr3vlem1  30160  frgrwopreg  30210  frgrregorufr  30212  frgrregord013  30282  9p10ne21fool  30358  satffunlem1lem1  35145  satffunlem2lem1  35147  jath  35452  hbimtg  35535  meran1  36028  imsym1  36035  ordcmp  36064  bj-babygodel  36213  bj-ssbid2ALT  36272  wl-lem-nexmo  37167  wl-ax11-lem2  37186  nexmo1  37851  mopickr  37967  axc5c7toc7  38517  axc5c711toc7  38524  axc5c711to11  38525  ax12indi  38548  eu6w  42238  onsucf1olem  42843  dflim5  42902  ifpim23g  43069  clsk1indlem3  43617  pm10.53  43947  pm11.63  43976  axc5c4c711  43982  axc5c4c711toc5  43983  axc5c4c711toc7  43985  axc5c4c711to11  43986  3ornot23  44092  notnotrALT  44112  hbimpg  44137  hbimpgVD  44487  notnotrALTVD  44498  climxrre  45278  liminf0  45321  prprelprb  46996  prminf2  47067  nn0o1gt2ALTV  47173  nn0oALTV  47175  gbowge7  47242  nnsum3primesle9  47273  bgoldbtbndlem1  47284  lindslinindsimp1  47713