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  2108  ax13dgen2  2139  ax13dgen4  2141  nfim1  2200  sbi2  2302  dfmoeu  2530  nexmo  2535  2mo  2642  axin2  2691  r19.35  3089  r19.35OLD  3090  r19.21v  3159  nrexrmo  3377  elab3gf  3654  elab3g  3655  moeq3  3686  dfss2  3935  ralidmw  4474  rzal  4475  ralidm  4478  opthpr  4818  opthprneg  4832  dfopif  4837  dvdemo1  5331  axprlem1  5381  axpr  5385  axprlem5OLD  5388  snopeqop  5469  weniso  7332  dfwe2  7753  ordunisuc2  7823  0mnnnnn0  12481  nn0ge2m1nn  12519  xrub  13279  injresinjlem  13755  fleqceilz  13823  addmodlteq  13918  fsuppmapnn0fiub0  13965  expnngt1  14213  hashnnn0genn0  14315  hashprb  14369  hash1snb  14391  hashgt12el  14394  hashgt12el2  14395  hash2prde  14442  hashge2el2dif  14452  hashge2el2difr  14453  dvdsaddre2b  16284  lcmf  16610  prmgaplem5  17033  cshwshashlem1  17073  acsfn  17627  symgfix2  19353  0ringnnzr  20441  mndifsplit  22530  symgmatr01lem  22547  xkopt  23549  umgrislfupgrlem  29056  lfgrwlkprop  29622  frgr3vlem1  30209  frgrwopreg  30259  frgrregorufr  30261  frgrregord013  30331  9p10ne21fool  30407  satffunlem1lem1  35396  satffunlem2lem1  35398  antnestlaw1  35685  antnestlaw2  35686  jath  35719  hbimtg  35801  meran1  36406  imsym1  36413  ordcmp  36442  bj-babygodel  36598  bj-ssbid2ALT  36658  wl-lem-nexmo  37562  wl-ax11-lem2  37581  nexmo1  38243  mopickr  38352  axc5c7toc7  38913  axc5c711toc7  38920  axc5c711to11  38921  ax12indi  38944  eu6w  42671  onsucf1olem  43266  dflim5  43325  ifpim23g  43491  clsk1indlem3  44039  pm10.53  44362  pm11.63  44391  axc5c4c711  44397  axc5c4c711toc5  44398  axc5c4c711toc7  44400  axc5c4c711to11  44401  3ornot23  44506  notnotrALT  44526  hbimpg  44551  hbimpgVD  44900  notnotrALTVD  44911  climxrre  45755  liminf0  45798  prprelprb  47522  prminf2  47593  nn0o1gt2ALTV  47699  nn0oALTV  47701  gbowge7  47768  nnsum3primesle9  47799  bgoldbtbndlem1  47810  usgrexmpl12ngrlic  48034  pgnbgreunbgrlem2  48111  lindslinindsimp1  48450