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  889  curryax  892  pm2.42  943  pm4.82  1024  pm5.71  1028  dedlem0b  1045  dedlemb  1047  cases2ALT  1049  cad0  1615  cad0OLD  1616  meredith  1639  tbw-bijust  1696  tbw-negdf  1697  nfntht  1791  19.38  1837  19.35  1876  sbn1  2107  ax13dgen2  2138  ax13dgen4  2140  nfim1  2200  sbi2  2306  dfmoeu  2539  nexmo  2544  2mo  2651  axin2  2700  r19.35  3114  r19.35OLD  3115  r19.21v  3186  nrexrmo  3409  elab3gf  3700  elab3g  3701  moeq3  3734  dfss2  3994  ralidmw  4531  rzal  4532  ralidm  4535  opthpr  4876  opthprneg  4889  dfopif  4894  dvdemo1  5391  axprlem1  5441  axprlem5  5445  snopeqop  5525  0nelopabOLD  5587  weniso  7390  dfwe2  7809  ordunisuc2  7881  0mnnnnn0  12585  nn0ge2m1nn  12622  xrub  13374  injresinjlem  13837  fleqceilz  13905  addmodlteq  13997  fsuppmapnn0fiub0  14044  expnngt1  14290  hashnnn0genn0  14392  hashprb  14446  hash1snb  14468  hashgt12el  14471  hashgt12el2  14472  hash2prde  14519  hashge2el2dif  14529  hashge2el2difr  14530  dvdsaddre2b  16355  lcmf  16680  prmgaplem5  17102  cshwshashlem1  17143  acsfn  17717  symgfix2  19458  0ringnnzr  20551  mndifsplit  22663  symgmatr01lem  22680  xkopt  23684  umgrislfupgrlem  29157  lfgrwlkprop  29723  frgr3vlem1  30305  frgrwopreg  30355  frgrregorufr  30357  frgrregord013  30427  9p10ne21fool  30503  satffunlem1lem1  35370  satffunlem2lem1  35372  jath  35687  hbimtg  35770  meran1  36377  imsym1  36384  ordcmp  36413  bj-babygodel  36569  bj-ssbid2ALT  36629  wl-lem-nexmo  37521  wl-ax11-lem2  37540  nexmo1  38203  mopickr  38319  axc5c7toc7  38869  axc5c711toc7  38876  axc5c711to11  38877  ax12indi  38900  eu6w  42631  onsucf1olem  43232  dflim5  43291  ifpim23g  43457  clsk1indlem3  44005  pm10.53  44335  pm11.63  44364  axc5c4c711  44370  axc5c4c711toc5  44371  axc5c4c711toc7  44373  axc5c4c711to11  44374  3ornot23  44480  notnotrALT  44500  hbimpg  44525  hbimpgVD  44875  notnotrALTVD  44886  climxrre  45671  liminf0  45714  prprelprb  47391  prminf2  47462  nn0o1gt2ALTV  47568  nn0oALTV  47570  gbowge7  47637  nnsum3primesle9  47668  bgoldbtbndlem1  47679  usgrexmpl12ngrlic  47854  lindslinindsimp1  48186