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  2107  ax13dgen2  2138  ax13dgen4  2140  nfim1  2199  sbi2  2302  dfmoeu  2535  nexmo  2540  2mo  2647  axin2  2696  r19.35  3095  r19.35OLD  3096  r19.21v  3165  nrexrmo  3380  elab3gf  3663  elab3g  3664  moeq3  3695  dfss2  3944  ralidmw  4483  rzal  4484  ralidm  4487  opthpr  4827  opthprneg  4841  dfopif  4846  dvdemo1  5343  axprlem1  5393  axpr  5397  axprlem5OLD  5400  snopeqop  5481  weniso  7346  dfwe2  7766  ordunisuc2  7837  0mnnnnn0  12531  nn0ge2m1nn  12569  xrub  13326  injresinjlem  13801  fleqceilz  13869  addmodlteq  13962  fsuppmapnn0fiub0  14009  expnngt1  14257  hashnnn0genn0  14359  hashprb  14413  hash1snb  14435  hashgt12el  14438  hashgt12el2  14439  hash2prde  14486  hashge2el2dif  14496  hashge2el2difr  14497  dvdsaddre2b  16324  lcmf  16650  prmgaplem5  17073  cshwshashlem1  17113  acsfn  17669  symgfix2  19395  0ringnnzr  20483  mndifsplit  22572  symgmatr01lem  22589  xkopt  23591  umgrislfupgrlem  29047  lfgrwlkprop  29613  frgr3vlem1  30200  frgrwopreg  30250  frgrregorufr  30252  frgrregord013  30322  9p10ne21fool  30398  satffunlem1lem1  35370  satffunlem2lem1  35372  jath  35688  hbimtg  35770  meran1  36375  imsym1  36382  ordcmp  36411  bj-babygodel  36567  bj-ssbid2ALT  36627  wl-lem-nexmo  37531  wl-ax11-lem2  37550  nexmo1  38212  mopickr  38327  axc5c7toc7  38877  axc5c711toc7  38884  axc5c711to11  38885  ax12indi  38908  eu6w  42646  onsucf1olem  43241  dflim5  43300  ifpim23g  43466  clsk1indlem3  44014  pm10.53  44338  pm11.63  44367  axc5c4c711  44373  axc5c4c711toc5  44374  axc5c4c711toc7  44376  axc5c4c711to11  44377  3ornot23  44482  notnotrALT  44502  hbimpg  44527  hbimpgVD  44876  notnotrALTVD  44887  climxrre  45727  liminf0  45770  prprelprb  47479  prminf2  47550  nn0o1gt2ALTV  47656  nn0oALTV  47658  gbowge7  47725  nnsum3primesle9  47756  bgoldbtbndlem1  47767  usgrexmpl12ngrlic  47991  lindslinindsimp1  48381