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  1615  meredith  1638  tbw-bijust  1695  tbw-negdf  1696  nfntht  1790  19.38  1836  19.35  1875  sbn1  2105  ax13dgen2  2136  ax13dgen4  2138  nfim1  2197  sbi2  2301  dfmoeu  2534  nexmo  2539  2mo  2646  axin2  2695  r19.35  3106  r19.35OLD  3107  r19.21v  3178  nrexrmo  3399  elab3gf  3687  elab3g  3688  moeq3  3721  dfss2  3981  ralidmw  4514  rzal  4515  ralidm  4518  opthpr  4856  opthprneg  4870  dfopif  4875  dvdemo1  5379  axprlem1  5429  axpr  5433  axprlem5OLD  5436  snopeqop  5516  weniso  7374  dfwe2  7793  ordunisuc2  7865  0mnnnnn0  12556  nn0ge2m1nn  12594  xrub  13351  injresinjlem  13823  fleqceilz  13891  addmodlteq  13984  fsuppmapnn0fiub0  14031  expnngt1  14277  hashnnn0genn0  14379  hashprb  14433  hash1snb  14455  hashgt12el  14458  hashgt12el2  14459  hash2prde  14506  hashge2el2dif  14516  hashge2el2difr  14517  dvdsaddre2b  16341  lcmf  16667  prmgaplem5  17089  cshwshashlem1  17130  acsfn  17704  symgfix2  19449  0ringnnzr  20542  mndifsplit  22658  symgmatr01lem  22675  xkopt  23679  umgrislfupgrlem  29154  lfgrwlkprop  29720  frgr3vlem1  30302  frgrwopreg  30352  frgrregorufr  30354  frgrregord013  30424  9p10ne21fool  30500  satffunlem1lem1  35387  satffunlem2lem1  35389  jath  35705  hbimtg  35788  meran1  36394  imsym1  36401  ordcmp  36430  bj-babygodel  36586  bj-ssbid2ALT  36646  wl-lem-nexmo  37548  wl-ax11-lem2  37567  nexmo1  38229  mopickr  38345  axc5c7toc7  38895  axc5c711toc7  38902  axc5c711to11  38903  ax12indi  38926  eu6w  42663  onsucf1olem  43260  dflim5  43319  ifpim23g  43485  clsk1indlem3  44033  pm10.53  44362  pm11.63  44391  axc5c4c711  44397  axc5c4c711toc5  44398  axc5c4c711toc7  44400  axc5c4c711to11  44401  3ornot23  44507  notnotrALT  44527  hbimpg  44552  hbimpgVD  44902  notnotrALTVD  44913  climxrre  45706  liminf0  45749  prprelprb  47442  prminf2  47513  nn0o1gt2ALTV  47619  nn0oALTV  47621  gbowge7  47688  nnsum3primesle9  47719  bgoldbtbndlem1  47730  usgrexmpl12ngrlic  47934  lindslinindsimp1  48303