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  890  curryax  893  pm2.42  942  pm4.82  1023  pm5.71  1027  dedlem0b  1044  dedlemb  1046  cases2ALT  1048  cad0  1620  cad0OLD  1621  meredith  1644  tbw-bijust  1701  tbw-negdf  1702  nfntht  1796  19.38  1842  19.35  1881  sbn1  2106  ax13dgen2  2135  ax13dgen4  2137  nfim1  2193  sbi2  2299  dfmoeu  2531  nexmo  2536  2mo  2645  axin2  2693  r19.35  3109  r19.35OLD  3110  r19.21v  3180  nrexrmo  3398  elab3gf  3675  elab3g  3676  moeq3  3709  ralidmw  4508  rzal  4509  ralidm  4512  opthpr  4853  opthprneg  4866  dfopif  4871  dvdemo1  5372  axprlem1  5422  axprlem5  5426  snopeqop  5507  0nelopabOLD  5569  weniso  7351  dfwe2  7761  ordunisuc2  7833  0mnnnnn0  12504  nn0ge2m1nn  12541  xrub  13291  injresinjlem  13752  fleqceilz  13819  addmodlteq  13911  fsuppmapnn0fiub0  13958  expnngt1  14204  hashnnn0genn0  14303  hashprb  14357  hash1snb  14379  hashgt12el  14382  hashgt12el2  14383  hash2prde  14431  hashge2el2dif  14441  hashge2el2difr  14442  dvdsaddre2b  16250  lcmf  16570  prmgaplem5  16988  cshwshashlem1  17029  acsfn  17603  symgfix2  19284  0ringnnzr  20302  mndifsplit  22138  symgmatr01lem  22155  xkopt  23159  umgrislfupgrlem  28413  lfgrwlkprop  28975  frgr3vlem1  29557  frgrwopreg  29607  frgrregorufr  29609  frgrregord013  29679  9p10ne21fool  29755  satffunlem1lem1  34424  satffunlem2lem1  34426  jath  34725  hbimtg  34809  meran1  35344  imsym1  35351  ordcmp  35380  bj-babygodel  35529  bj-ssbid2ALT  35588  wl-lem-nexmo  36480  wl-ax11-lem2  36496  nexmo1  37162  mopickr  37280  axc5c7toc7  37831  axc5c711toc7  37838  axc5c711to11  37839  ax12indi  37862  onsucf1olem  42068  dflim5  42127  ifpim23g  42294  clsk1indlem3  42842  pm10.53  43173  pm11.63  43202  axc5c4c711  43208  axc5c4c711toc5  43209  axc5c4c711toc7  43211  axc5c4c711to11  43212  3ornot23  43318  notnotrALT  43338  hbimpg  43363  hbimpgVD  43713  notnotrALTVD  43724  climxrre  44514  liminf0  44557  prprelprb  46233  prminf2  46304  nn0o1gt2ALTV  46410  nn0oALTV  46412  gbowge7  46479  nnsum3primesle9  46510  bgoldbtbndlem1  46521  lindslinindsimp1  47186