Theorem pm2.21 124

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 125 and its associated inference is pm2.21i 120. (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 23	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	pm2.21d 122	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  125  jarl  126  jarli  127  pm2.18d  128  simplim  168  orel2  903  curryax  906  pm2.42  957  pm4.82  1039  pm5.71  1043  dedlem0b  1058  dedlemb  1060  cases2ALT  1062  cad0  1641  meredith  1664  tbw-bijust  1721  tbw-negdf  1722  nfntht  1816  19.38  1862  19.35  1900  sbrimvw  2127  sbn1  2144  ax13dgen2  2175  ax13dgen4  2177  nfim1  2237  sbi2  2339  dfmoeu  2565  nexmo  2571  2mo  2678  axin2  2726  r19.35  3123  r19.21v  3190  nrexrmo  3389  elab3gf  3646  elab3g  3647  moeq3  3678  dfss2  3925  rzal  4451  falseral0  4471  ralidmw  4473  ralidm  4474  opthpr  4811  opthprneg  4825  dfopif  4830  dvdemo1  5334  axprlem1  5384  axpr  5388  axprlem1OLD  5389  axprlem5OLD  5392  axprg  5398  snopeqop  5479  weniso  7342  dfwe2  7761  ordunisuc2  7828  0mnnnnn0  12524  nn0ge2m1nn  12562  xrub  13326  injresinjlem  13807  fleqceilz  13875  addmodlteq  13970  fsuppmapnn0fiub0  14017  expnngt1  14265  hashnnn0genn0  14367  hashprb  14421  hash1snb  14444  hashgt12el  14447  hashgt12el2  14448  hash2prde  14495  hashge2el2dif  14505  hashge2el2difr  14506  dvdsaddre2b  16353  lcmf  16679  prmgaplem5  17103  cshwshashlem1  17143  acsfn  17703  symgfix2  19474  0ringnnzr  20597  mndifsplit  22750  symgmatr01lem  22767  xkopt  23769  umgrislfupgrlem  29377  lfgrwlkprop  29940  frgr3vlem1  30529  frgrwopreg  30579  frgrregorufr  30581  frgrregord013  30651  9p10ne21fool  30727  satffunlem1lem1  35760  satffunlem2lem1  35762  antnestlaw1  36049  antnestlaw2  36050  jath  36083  hbimtg  36162  meran1  36779  imsym1  36786  ordcmp  36815  dfttc4lem2  36897  mh-infprim1bi  36914  bj-babygodel  37053  bj-ssbid2ALT  37142  wl-lem-nexmo  38077  nexmo1  38755  mopickr  38877  axc5c7toc7  39544  axc5c711toc7  39551  axc5c711to11  39552  ax12indi  39575  eu6w  43265  onsucf1olem  43854  dflim5  43913  ifpim23g  44078  clsk1indlem3  44626  pm10.53  44935  pm11.63  44964  axc5c4c711  44970  axc5c4c711toc5  44971  axc5c4c711toc7  44973  axc5c4c711to11  44974  3ornot23  45077  notnotrALT  45097  hbimpg  45122  hbimpgVD  45471  notnotrALTVD  45482  climxrre  46323  liminf0  46366  quantgodelALT  47448  prprelprb  48122  prminf2  48196  nn0o1gt2ALTV  48315  nn0oALTV  48317  gbowge7  48384  nnsum3primesle9  48415  bgoldbtbndlem1  48426  usgrexmpl12ngrlic  48660  pgnbgreunbgrlem2  48738  lindslinindsimp1  49089