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  944  pm4.82  1025  pm5.71  1029  dedlem0b  1044  dedlemb  1046  cases2ALT  1048  cad0  1618  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  nfntht  1793  19.38  1839  19.35  1877  sbn1  2107  ax13dgen2  2138  ax13dgen4  2140  nfim1  2199  sbi2  2302  dfmoeu  2535  nexmo  2540  2mo  2647  axin2  2696  r19.35  3095  r19.35OLD  3096  r19.21v  3165  nrexrmo  3380  elab3gf  3663  elab3g  3664  moeq3  3695  dfss2  3944  ralidmw  4483  rzal  4484  ralidm  4487  opthpr  4827  opthprneg  4841  dfopif  4846  dvdemo1  5343  axprlem1  5393  axpr  5397  axprlem5OLD  5400  snopeqop  5481  weniso  7347  dfwe2  7768  ordunisuc2  7839  0mnnnnn0  12533  nn0ge2m1nn  12571  xrub  13328  injresinjlem  13803  fleqceilz  13871  addmodlteq  13964  fsuppmapnn0fiub0  14011  expnngt1  14259  hashnnn0genn0  14361  hashprb  14415  hash1snb  14437  hashgt12el  14440  hashgt12el2  14441  hash2prde  14488  hashge2el2dif  14498  hashge2el2difr  14499  dvdsaddre2b  16326  lcmf  16652  prmgaplem5  17075  cshwshashlem1  17115  acsfn  17671  symgfix2  19397  0ringnnzr  20485  mndifsplit  22574  symgmatr01lem  22591  xkopt  23593  umgrislfupgrlem  29101  lfgrwlkprop  29667  frgr3vlem1  30254  frgrwopreg  30304  frgrregorufr  30306  frgrregord013  30376  9p10ne21fool  30452  satffunlem1lem1  35424  satffunlem2lem1  35426  jath  35742  hbimtg  35824  meran1  36429  imsym1  36436  ordcmp  36465  bj-babygodel  36621  bj-ssbid2ALT  36681  wl-lem-nexmo  37585  wl-ax11-lem2  37604  nexmo1  38266  mopickr  38381  axc5c7toc7  38931  axc5c711toc7  38938  axc5c711to11  38939  ax12indi  38962  eu6w  42699  onsucf1olem  43294  dflim5  43353  ifpim23g  43519  clsk1indlem3  44067  pm10.53  44390  pm11.63  44419  axc5c4c711  44425  axc5c4c711toc5  44426  axc5c4c711toc7  44428  axc5c4c711to11  44429  3ornot23  44534  notnotrALT  44554  hbimpg  44579  hbimpgVD  44928  notnotrALTVD  44939  climxrre  45779  liminf0  45822  prprelprb  47531  prminf2  47602  nn0o1gt2ALTV  47708  nn0oALTV  47710  gbowge7  47777  nnsum3primesle9  47808  bgoldbtbndlem1  47819  usgrexmpl12ngrlic  48043  lindslinindsimp1  48433