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  896  curryax  899  pm2.42  950  pm4.82  1031  pm5.71  1035  dedlem0b  1050  dedlemb  1052  cases2ALT  1054  cad0  1625  meredith  1648  tbw-bijust  1705  tbw-negdf  1706  nfntht  1800  19.38  1846  19.35  1884  sbn1  2118  ax13dgen2  2149  ax13dgen4  2151  nfim1  2211  sbi2  2313  dfmoeu  2539  nexmo  2545  2mo  2652  axin2  2701  r19.35  3098  r19.21v  3165  nrexrmo  3364  elab3gf  3629  elab3g  3630  moeq3  3660  dfss2  3908  rzal  4429  falseral0  4449  ralidmw  4451  ralidm  4452  opthpr  4789  opthprneg  4803  dfopif  4808  dvdemo1  5309  axprlem1  5359  axpr  5363  axprlem1OLD  5364  axprlem5OLD  5367  axprg  5373  snopeqop  5454  weniso  7305  dfwe2  7724  ordunisuc2  7791  0mnnnnn0  12467  nn0ge2m1nn  12505  xrub  13262  injresinjlem  13743  fleqceilz  13811  addmodlteq  13906  fsuppmapnn0fiub0  13953  expnngt1  14201  hashnnn0genn0  14303  hashprb  14357  hash1snb  14379  hashgt12el  14382  hashgt12el2  14383  hash2prde  14430  hashge2el2dif  14440  hashge2el2difr  14441  dvdsaddre2b  16274  lcmf  16600  prmgaplem5  17024  cshwshashlem1  17064  acsfn  17623  symgfix2  19389  0ringnnzr  20504  mndifsplit  22626  symgmatr01lem  22643  xkopt  23645  umgrislfupgrlem  29216  lfgrwlkprop  29779  frgr3vlem1  30368  frgrwopreg  30418  frgrregorufr  30420  frgrregord013  30490  9p10ne21fool  30566  satffunlem1lem1  35637  satffunlem2lem1  35639  antnestlaw1  35926  antnestlaw2  35927  jath  35960  hbimtg  36039  meran1  36646  imsym1  36653  ordcmp  36682  dfttc4lem2  36764  mh-infprim1bi  36781  bj-babygodel  36921  bj-ssbid2ALT  37010  wl-lem-nexmo  37945  nexmo1  38623  mopickr  38745  axc5c7toc7  39412  axc5c711toc7  39419  axc5c711to11  39420  ax12indi  39443  eu6w  43133  onsucf1olem  43722  dflim5  43781  ifpim23g  43946  clsk1indlem3  44494  pm10.53  44817  pm11.63  44846  axc5c4c711  44852  axc5c4c711toc5  44853  axc5c4c711toc7  44855  axc5c4c711to11  44856  3ornot23  44960  notnotrALT  44980  hbimpg  45005  hbimpgVD  45354  notnotrALTVD  45365  climxrre  46200  liminf0  46243  quantgodelALT  47325  prprelprb  47999  prminf2  48073  nn0o1gt2ALTV  48192  nn0oALTV  48194  gbowge7  48261  nnsum3primesle9  48292  bgoldbtbndlem1  48303  usgrexmpl12ngrlic  48537  pgnbgreunbgrlem2  48615  lindslinindsimp1  48955