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  888  curryax  891  pm2.42  940  pm4.82  1021  pm5.71  1025  dedlem0b  1042  dedlemb  1044  cases2ALT  1046  cad0  1620  cad0OLD  1621  meredith  1644  tbw-bijust  1701  tbw-negdf  1702  nfntht  1796  19.38  1841  19.35  1880  sbn1  2105  ax13dgen2  2134  ax13dgen4  2136  nfim1  2192  sbi2  2299  dfmoeu  2536  nexmo  2541  2mo  2650  axin2  2698  r19.21v  3113  r19.35  3271  nrexrmo  3366  elab3gf  3615  elab3g  3616  moeq3  3647  ralidmw  4438  rzal  4439  ralidm  4442  opthpr  4782  opthprneg  4795  dfopifOLD  4801  dvdemo1  5296  axprlem1  5346  axprlem5  5350  snopeqop  5420  0nelopabOLD  5481  weniso  7225  dfwe2  7624  ordunisuc2  7691  0mnnnnn0  12265  nn0ge2m1nn  12302  xrub  13046  injresinjlem  13507  fleqceilz  13574  addmodlteq  13666  fsuppmapnn0fiub0  13713  expnngt1  13956  hashnnn0genn0  14057  hashprb  14112  hash1snb  14134  hashgt12el  14137  hashgt12el2  14138  hash2prde  14184  hashge2el2dif  14194  hashge2el2difr  14195  dvdsaddre2b  16016  lcmf  16338  prmgaplem5  16756  cshwshashlem1  16797  acsfn  17368  symgfix2  19024  0ringnnzr  20540  mndifsplit  21785  symgmatr01lem  21802  xkopt  22806  umgrislfupgrlem  27492  lfgrwlkprop  28055  frgr3vlem1  28637  frgrwopreg  28687  frgrregorufr  28689  frgrregord013  28759  9p10ne21fool  28835  satffunlem1lem1  33364  satffunlem2lem1  33366  jath  33672  hbimtg  33782  meran1  34600  imsym1  34607  ordcmp  34636  bj-babygodel  34785  bj-ssbid2ALT  34844  wl-lem-nexmo  35722  wl-ax11-lem2  35737  nexmo1  36386  axc5c7toc7  36927  axc5c711toc7  36934  axc5c711to11  36935  ax12indi  36958  ifpim23g  41102  clsk1indlem3  41653  pm10.53  41984  pm11.63  42013  axc5c4c711  42019  axc5c4c711toc5  42020  axc5c4c711toc7  42022  axc5c4c711to11  42023  3ornot23  42129  notnotrALT  42149  hbimpg  42174  hbimpgVD  42524  notnotrALTVD  42535  climxrre  43291  liminf0  43334  prprelprb  44969  prminf2  45040  nn0o1gt2ALTV  45146  nn0oALTV  45148  gbowge7  45215  nnsum3primesle9  45246  bgoldbtbndlem1  45257  lindslinindsimp1  45798