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  28382  lfgrwlkprop  28944  frgr3vlem1  29526  frgrwopreg  29576  frgrregorufr  29578  frgrregord013  29648  9p10ne21fool  29724  satffunlem1lem1  34393  satffunlem2lem1  34395  jath  34694  hbimtg  34778  meran1  35296  imsym1  35303  ordcmp  35332  bj-babygodel  35481  bj-ssbid2ALT  35540  wl-lem-nexmo  36432  wl-ax11-lem2  36448  nexmo1  37114  mopickr  37232  axc5c7toc7  37783  axc5c711toc7  37790  axc5c711to11  37791  ax12indi  37814  onsucf1olem  42020  dflim5  42079  ifpim23g  42246  clsk1indlem3  42794  pm10.53  43125  pm11.63  43154  axc5c4c711  43160  axc5c4c711toc5  43161  axc5c4c711toc7  43163  axc5c4c711to11  43164  3ornot23  43270  notnotrALT  43290  hbimpg  43315  hbimpgVD  43665  notnotrALTVD  43676  climxrre  44466  liminf0  44509  prprelprb  46185  prminf2  46256  nn0o1gt2ALTV  46362  nn0oALTV  46364  gbowge7  46431  nnsum3primesle9  46462  bgoldbtbndlem1  46473  lindslinindsimp1  47138