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  889  curryax  892  pm2.42  941  pm4.82  1022  pm5.71  1026  dedlem0b  1043  dedlemb  1045  cases2ALT  1047  cad0  1619  cad0OLD  1620  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  nfntht  1795  19.38  1841  19.35  1880  sbn1  2105  ax13dgen2  2134  ax13dgen4  2136  nfim1  2192  sbi2  2298  dfmoeu  2530  nexmo  2535  2mo  2644  axin2  2692  r19.35  3108  r19.35OLD  3109  r19.21v  3179  nrexrmo  3397  elab3gf  3674  elab3g  3675  moeq3  3708  ralidmw  4507  rzal  4508  ralidm  4511  opthpr  4852  opthprneg  4865  dfopif  4870  dvdemo1  5371  axprlem1  5421  axprlem5  5425  snopeqop  5506  0nelopabOLD  5568  weniso  7353  dfwe2  7763  ordunisuc2  7835  0mnnnnn0  12508  nn0ge2m1nn  12545  xrub  13295  injresinjlem  13756  fleqceilz  13823  addmodlteq  13915  fsuppmapnn0fiub0  13962  expnngt1  14208  hashnnn0genn0  14307  hashprb  14361  hash1snb  14383  hashgt12el  14386  hashgt12el2  14387  hash2prde  14435  hashge2el2dif  14445  hashge2el2difr  14446  dvdsaddre2b  16254  lcmf  16574  prmgaplem5  16992  cshwshashlem1  17033  acsfn  17607  symgfix2  19325  0ringnnzr  20414  mndifsplit  22358  symgmatr01lem  22375  xkopt  23379  umgrislfupgrlem  28637  lfgrwlkprop  29199  frgr3vlem1  29781  frgrwopreg  29831  frgrregorufr  29833  frgrregord013  29903  9p10ne21fool  29979  satffunlem1lem1  34679  satffunlem2lem1  34681  jath  34986  hbimtg  35070  meran1  35599  imsym1  35606  ordcmp  35635  bj-babygodel  35784  bj-ssbid2ALT  35843  wl-lem-nexmo  36735  wl-ax11-lem2  36751  nexmo1  37417  mopickr  37535  axc5c7toc7  38086  axc5c711toc7  38093  axc5c711to11  38094  ax12indi  38117  onsucf1olem  42322  dflim5  42381  ifpim23g  42548  clsk1indlem3  43096  pm10.53  43427  pm11.63  43456  axc5c4c711  43462  axc5c4c711toc5  43463  axc5c4c711toc7  43465  axc5c4c711to11  43466  3ornot23  43572  notnotrALT  43592  hbimpg  43617  hbimpgVD  43967  notnotrALTVD  43978  climxrre  44765  liminf0  44808  prprelprb  46484  prminf2  46555  nn0o1gt2ALTV  46661  nn0oALTV  46663  gbowge7  46730  nnsum3primesle9  46761  bgoldbtbndlem1  46772  lindslinindsimp1  47226