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  891  curryax  894  pm2.42  945  pm4.82  1026  pm5.71  1030  dedlem0b  1045  dedlemb  1047  cases2ALT  1049  cad0  1620  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  nfntht  1795  19.38  1841  19.35  1879  sbn1  2113  ax13dgen2  2144  ax13dgen4  2146  nfim1  2207  sbi2  2309  dfmoeu  2536  nexmo  2542  2mo  2649  axin2  2698  r19.35  3096  r19.21v  3163  nrexrmo  3371  elab3gf  3641  elab3g  3642  moeq3  3672  dfss2  3921  rzal  4449  falseral0  4469  ralidmw  4471  ralidm  4472  opthpr  4809  opthprneg  4823  dfopif  4828  dvdemo1  5320  axprlem1  5370  axpr  5374  axprlem5OLD  5377  axprg  5383  snopeqop  5462  weniso  7310  dfwe2  7729  ordunisuc2  7796  0mnnnnn0  12445  nn0ge2m1nn  12483  xrub  13239  injresinjlem  13718  fleqceilz  13786  addmodlteq  13881  fsuppmapnn0fiub0  13928  expnngt1  14176  hashnnn0genn0  14278  hashprb  14332  hash1snb  14354  hashgt12el  14357  hashgt12el2  14358  hash2prde  14405  hashge2el2dif  14415  hashge2el2difr  14416  dvdsaddre2b  16246  lcmf  16572  prmgaplem5  16995  cshwshashlem1  17035  acsfn  17594  symgfix2  19357  0ringnnzr  20470  mndifsplit  22592  symgmatr01lem  22609  xkopt  23611  umgrislfupgrlem  29207  lfgrwlkprop  29771  frgr3vlem1  30360  frgrwopreg  30410  frgrregorufr  30412  frgrregord013  30482  9p10ne21fool  30558  satffunlem1lem1  35615  satffunlem2lem1  35617  antnestlaw1  35904  antnestlaw2  35905  jath  35938  hbimtg  36017  meran1  36624  imsym1  36631  ordcmp  36660  bj-babygodel  36824  bj-ssbid2ALT  36902  wl-lem-nexmo  37816  nexmo1  38494  mopickr  38616  axc5c7toc7  39283  axc5c711toc7  39290  axc5c711to11  39291  ax12indi  39314  eu6w  43028  onsucf1olem  43621  dflim5  43680  ifpim23g  43845  clsk1indlem3  44393  pm10.53  44716  pm11.63  44745  axc5c4c711  44751  axc5c4c711toc5  44752  axc5c4c711toc7  44754  axc5c4c711to11  44755  3ornot23  44859  notnotrALT  44879  hbimpg  44904  hbimpgVD  45253  notnotrALTVD  45264  climxrre  46102  liminf0  46145  prprelprb  47871  prminf2  47942  nn0o1gt2ALTV  48048  nn0oALTV  48050  gbowge7  48117  nnsum3primesle9  48148  bgoldbtbndlem1  48159  usgrexmpl12ngrlic  48393  pgnbgreunbgrlem2  48471  lindslinindsimp1  48811