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  3087  r19.21v  3154  nrexrmo  3366  elab3gf  3642  elab3g  3643  moeq3  3674  dfss2  3923  ralidmw  4461  rzal  4462  ralidm  4465  opthpr  4805  opthprneg  4819  dfopif  4824  dvdemo1  5315  axprlem1  5365  axpr  5369  axprlem5OLD  5372  snopeqop  5453  weniso  7295  dfwe2  7714  ordunisuc2  7784  0mnnnnn0  12434  nn0ge2m1nn  12472  xrub  13232  injresinjlem  13708  fleqceilz  13776  addmodlteq  13871  fsuppmapnn0fiub0  13918  expnngt1  14166  hashnnn0genn0  14268  hashprb  14322  hash1snb  14344  hashgt12el  14347  hashgt12el2  14348  hash2prde  14395  hashge2el2dif  14405  hashge2el2difr  14406  dvdsaddre2b  16236  lcmf  16562  prmgaplem5  16985  cshwshashlem1  17025  acsfn  17583  symgfix2  19313  0ringnnzr  20428  mndifsplit  22539  symgmatr01lem  22556  xkopt  23558  umgrislfupgrlem  29085  lfgrwlkprop  29649  frgr3vlem1  30235  frgrwopreg  30285  frgrregorufr  30287  frgrregord013  30357  9p10ne21fool  30433  satffunlem1lem1  35374  satffunlem2lem1  35376  antnestlaw1  35663  antnestlaw2  35664  jath  35697  hbimtg  35779  meran1  36384  imsym1  36391  ordcmp  36420  bj-babygodel  36576  bj-ssbid2ALT  36636  wl-lem-nexmo  37540  wl-ax11-lem2  37559  nexmo1  38221  mopickr  38330  axc5c7toc7  38891  axc5c711toc7  38898  axc5c711to11  38899  ax12indi  38922  eu6w  42649  onsucf1olem  43243  dflim5  43302  ifpim23g  43468  clsk1indlem3  44016  pm10.53  44339  pm11.63  44368  axc5c4c711  44374  axc5c4c711toc5  44375  axc5c4c711toc7  44377  axc5c4c711to11  44378  3ornot23  44483  notnotrALT  44503  hbimpg  44528  hbimpgVD  44877  notnotrALTVD  44888  climxrre  45732  liminf0  45775  prprelprb  47502  prminf2  47573  nn0o1gt2ALTV  47679  nn0oALTV  47681  gbowge7  47748  nnsum3primesle9  47779  bgoldbtbndlem1  47790  usgrexmpl12ngrlic  48024  pgnbgreunbgrlem2  48102  lindslinindsimp1  48443