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  pm2.18OLD  129  simplim  169  orel2  887  curryax  890  pm2.42  939  pm4.82  1020  pm5.71  1024  dedlem0b  1039  dedlemb  1041  cases2ALT  1043  cad0  1618  meredith  1642  tbw-bijust  1699  tbw-negdf  1700  nfntht  1794  19.38  1839  19.35  1878  ax13dgen2  2142  ax13dgen4  2144  nfim1  2199  sbi2  2310  sbi2vOLD  2324  sbi2ALT  2607  dfmoeu  2618  nexmo  2623  2mo  2733  axin2  2782  r19.35  3341  nrexrmo  3435  elab3gf  3672  moeq3  3703  opthpr  4782  preqsnd  4789  opthprneg  4795  dfopif  4800  dvdemo1  5274  axprlem1  5324  axprlem5  5328  snopeqop  5396  0nelopab  5452  weniso  7107  dfwe2  7496  ordunisuc2  7559  0mnnnnn0  11930  nn0ge2m1nn  11965  xrub  12706  injresinjlem  13158  fleqceilz  13223  addmodlteq  13315  fsuppmapnn0fiub0  13362  expnngt1  13603  hashnnn0genn0  13704  hashprb  13759  hash1snb  13781  hashgt12el  13784  hashgt12el2  13785  hash2prde  13829  hashge2el2dif  13839  hashge2el2difr  13840  dvdsaddre2b  15657  lcmf  15977  prmgaplem5  16391  cshwshashlem1  16429  acsfn  16930  symgfix2  18544  0ringnnzr  20042  mndifsplit  21245  symgmatr01lem  21262  xkopt  22263  umgrislfupgrlem  26907  lfgrwlkprop  27469  frgr3vlem1  28052  frgrwopreg  28102  frgrregorufr  28104  frgrregord013  28174  9p10ne21fool  28250  satffunlem1lem1  32649  satffunlem2lem1  32651  jath  32958  hbimtg  33051  meran1  33759  imsym1  33766  ordcmp  33795  bj-babygodel  33937  bj-ssbid2ALT  33996  wl-lem-nexmo  34818  wl-ax11-lem2  34833  nexmo1  35523  axc5c7toc7  36064  axc5c711toc7  36071  axc5c711to11  36072  ax12indi  36095  sbn1  39122  ifpim23g  39881  clsk1indlem3  40413  pm10.53  40718  pm11.63  40747  axc5c4c711  40753  axc5c4c711toc5  40754  axc5c4c711toc7  40756  axc5c4c711to11  40757  3ornot23  40863  notnotrALT  40883  hbimpg  40908  hbimpgVD  41258  notnotrALTVD  41269  climxrre  42051  liminf0  42094  prprelprb  43699  prminf2  43770  nn0o1gt2ALTV  43879  nn0oALTV  43881  gbowge7  43948  nnsum3primesle9  43979  bgoldbtbndlem1  43990  lindslinindsimp1  44532