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  887  curryax  890  pm2.42  939  pm4.82  1020  pm5.71  1024  dedlem0b  1041  dedlemb  1043  cases2ALT  1045  cad0  1621  cad0OLD  1622  meredith  1645  tbw-bijust  1702  tbw-negdf  1703  nfntht  1797  19.38  1842  19.35  1881  sbn1  2107  ax13dgen2  2136  ax13dgen4  2138  nfim1  2195  sbi2  2302  dfmoeu  2536  nexmo  2541  2mo  2650  axin2  2698  r19.35  3268  nrexrmo  3356  elab3gf  3608  elab3g  3609  moeq3  3642  ralidmw  4435  rzal  4436  ralidm  4439  opthpr  4779  opthprneg  4792  dfopifOLD  4798  dvdemo1  5291  axprlem1  5341  axprlem5  5345  snopeqop  5414  0nelopabOLD  5472  weniso  7205  dfwe2  7602  ordunisuc2  7666  0mnnnnn0  12195  nn0ge2m1nn  12232  xrub  12975  injresinjlem  13435  fleqceilz  13502  addmodlteq  13594  fsuppmapnn0fiub0  13641  expnngt1  13884  hashnnn0genn0  13985  hashprb  14040  hash1snb  14062  hashgt12el  14065  hashgt12el2  14066  hash2prde  14112  hashge2el2dif  14122  hashge2el2difr  14123  dvdsaddre2b  15944  lcmf  16266  prmgaplem5  16684  cshwshashlem1  16725  acsfn  17285  symgfix2  18939  0ringnnzr  20453  mndifsplit  21693  symgmatr01lem  21710  xkopt  22714  umgrislfupgrlem  27395  lfgrwlkprop  27957  frgr3vlem1  28538  frgrwopreg  28588  frgrregorufr  28590  frgrregord013  28660  9p10ne21fool  28736  satffunlem1lem1  33264  satffunlem2lem1  33266  jath  33574  hbimtg  33688  meran1  34527  imsym1  34534  ordcmp  34563  bj-babygodel  34712  bj-ssbid2ALT  34771  wl-lem-nexmo  35649  wl-ax11-lem2  35664  nexmo1  36313  axc5c7toc7  36854  axc5c711toc7  36861  axc5c711to11  36862  ax12indi  36885  ifpim23g  41000  clsk1indlem3  41542  pm10.53  41873  pm11.63  41902  axc5c4c711  41908  axc5c4c711toc5  41909  axc5c4c711toc7  41911  axc5c4c711to11  41912  3ornot23  42018  notnotrALT  42038  hbimpg  42063  hbimpgVD  42413  notnotrALTVD  42424  climxrre  43181  liminf0  43224  prprelprb  44857  prminf2  44928  nn0o1gt2ALTV  45034  nn0oALTV  45036  gbowge7  45103  nnsum3primesle9  45134  bgoldbtbndlem1  45145  lindslinindsimp1  45686