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  2529  nexmo  2534  2mo  2641  axin2  2690  r19.35  3088  r19.35OLD  3089  r19.21v  3158  nrexrmo  3375  elab3gf  3651  elab3g  3652  moeq3  3683  dfss2  3932  ralidmw  4471  rzal  4472  ralidm  4475  opthpr  4815  opthprneg  4829  dfopif  4834  dvdemo1  5328  axprlem1  5378  axpr  5382  axprlem5OLD  5385  snopeqop  5466  weniso  7329  dfwe2  7750  ordunisuc2  7820  0mnnnnn0  12474  nn0ge2m1nn  12512  xrub  13272  injresinjlem  13748  fleqceilz  13816  addmodlteq  13911  fsuppmapnn0fiub0  13958  expnngt1  14206  hashnnn0genn0  14308  hashprb  14362  hash1snb  14384  hashgt12el  14387  hashgt12el2  14388  hash2prde  14435  hashge2el2dif  14445  hashge2el2difr  14446  dvdsaddre2b  16277  lcmf  16603  prmgaplem5  17026  cshwshashlem1  17066  acsfn  17620  symgfix2  19346  0ringnnzr  20434  mndifsplit  22523  symgmatr01lem  22540  xkopt  23542  umgrislfupgrlem  29049  lfgrwlkprop  29615  frgr3vlem1  30202  frgrwopreg  30252  frgrregorufr  30254  frgrregord013  30324  9p10ne21fool  30400  satffunlem1lem1  35389  satffunlem2lem1  35391  antnestlaw1  35678  antnestlaw2  35679  jath  35712  hbimtg  35794  meran1  36399  imsym1  36406  ordcmp  36435  bj-babygodel  36591  bj-ssbid2ALT  36651  wl-lem-nexmo  37555  wl-ax11-lem2  37574  nexmo1  38236  mopickr  38345  axc5c7toc7  38906  axc5c711toc7  38913  axc5c711to11  38914  ax12indi  38937  eu6w  42664  onsucf1olem  43259  dflim5  43318  ifpim23g  43484  clsk1indlem3  44032  pm10.53  44355  pm11.63  44384  axc5c4c711  44390  axc5c4c711toc5  44391  axc5c4c711toc7  44393  axc5c4c711to11  44394  3ornot23  44499  notnotrALT  44519  hbimpg  44544  hbimpgVD  44893  notnotrALTVD  44904  climxrre  45748  liminf0  45791  prprelprb  47518  prminf2  47589  nn0o1gt2ALTV  47695  nn0oALTV  47697  gbowge7  47764  nnsum3primesle9  47795  bgoldbtbndlem1  47806  usgrexmpl12ngrlic  48030  pgnbgreunbgrlem2  48107  lindslinindsimp1  48446