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  4812  opthprneg  4826  dfopif  4831  dvdemo1  5335  axprlem1  5385  axpr  5389  axprlem1OLD  5390  axprlem5OLD  5393  axprg  5399  snopeqop  5480  weniso  7342  dfwe2  7761  ordunisuc2  7828  0mnnnnn0  12527  nn0ge2m1nn  12565  xrub  13329  injresinjlem  13810  fleqceilz  13878  addmodlteq  13973  fsuppmapnn0fiub0  14020  expnngt1  14268  hashnnn0genn0  14370  hashprb  14424  hash1snb  14446  hashgt12el  14449  hashgt12el2  14450  hash2prde  14497  hashge2el2dif  14507  hashge2el2difr  14508  dvdsaddre2b  16355  lcmf  16681  prmgaplem5  17105  cshwshashlem1  17145  acsfn  17705  symgfix2  19477  0ringnnzr  20600  mndifsplit  22754  symgmatr01lem  22771  xkopt  23773  umgrislfupgrlem  29381  lfgrwlkprop  29944  frgr3vlem1  30533  frgrwopreg  30583  frgrregorufr  30585  frgrregord013  30655  9p10ne21fool  30731  satffunlem1lem1  35765  satffunlem2lem1  35767  antnestlaw1  36054  antnestlaw2  36055  jath  36088  hbimtg  36167  meran1  36784  imsym1  36791  ordcmp  36820  dfttc4lem2  36902  mh-infprim1bi  36919  bj-babygodel  37058  bj-ssbid2ALT  37147  wl-lem-nexmo  38082  nexmo1  38760  mopickr  38882  axc5c7toc7  39549  axc5c711toc7  39556  axc5c711to11  39557  ax12indi  39580  eu6w  43270  onsucf1olem  43859  dflim5  43918  ifpim23g  44083  clsk1indlem3  44631  pm10.53  44940  pm11.63  44969  axc5c4c711  44975  axc5c4c711toc5  44976  axc5c4c711toc7  44978  axc5c4c711to11  44979  3ornot23  45083  notnotrALT  45103  hbimpg  45128  hbimpgVD  45477  notnotrALTVD  45488  climxrre  46322  liminf0  46365  quantgodelALT  47447  prprelprb  48121  prminf2  48195  nn0o1gt2ALTV  48314  nn0oALTV  48316  gbowge7  48383  nnsum3primesle9  48414  bgoldbtbndlem1  48425  usgrexmpl12ngrlic  48659  pgnbgreunbgrlem2  48737  lindslinindsimp1  49088