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  1619  meredith  1642  tbw-bijust  1699  tbw-negdf  1700  nfntht  1794  19.38  1840  19.35  1878  sbn1  2112  ax13dgen2  2143  ax13dgen4  2145  nfim1  2204  sbi2  2306  dfmoeu  2533  nexmo  2538  2mo  2645  axin2  2694  r19.35  3091  r19.21v  3158  nrexrmo  3366  elab3gf  3636  elab3g  3637  moeq3  3667  dfss2  3916  ralidmw  4457  rzal  4458  ralidm  4461  opthpr  4802  opthprneg  4816  dfopif  4821  dvdemo1  5313  axprlem1  5363  axpr  5367  axprlem5OLD  5370  snopeqop  5449  weniso  7294  dfwe2  7713  ordunisuc2  7780  0mnnnnn0  12420  nn0ge2m1nn  12458  xrub  13213  injresinjlem  13692  fleqceilz  13760  addmodlteq  13855  fsuppmapnn0fiub0  13902  expnngt1  14150  hashnnn0genn0  14252  hashprb  14306  hash1snb  14328  hashgt12el  14331  hashgt12el2  14332  hash2prde  14379  hashge2el2dif  14389  hashge2el2difr  14390  dvdsaddre2b  16220  lcmf  16546  prmgaplem5  16969  cshwshashlem1  17009  acsfn  17567  symgfix2  19330  0ringnnzr  20442  mndifsplit  22552  symgmatr01lem  22569  xkopt  23571  umgrislfupgrlem  29102  lfgrwlkprop  29666  frgr3vlem1  30255  frgrwopreg  30305  frgrregorufr  30307  frgrregord013  30377  9p10ne21fool  30453  satffunlem1lem1  35467  satffunlem2lem1  35469  antnestlaw1  35756  antnestlaw2  35757  jath  35790  hbimtg  35869  meran1  36476  imsym1  36483  ordcmp  36512  bj-babygodel  36668  bj-ssbid2ALT  36728  wl-lem-nexmo  37632  nexmo1  38304  mopickr  38415  axc5c7toc7  39032  axc5c711toc7  39039  axc5c711to11  39040  ax12indi  39063  eu6w  42794  onsucf1olem  43387  dflim5  43446  ifpim23g  43612  clsk1indlem3  44160  pm10.53  44483  pm11.63  44512  axc5c4c711  44518  axc5c4c711toc5  44519  axc5c4c711toc7  44521  axc5c4c711to11  44522  3ornot23  44626  notnotrALT  44646  hbimpg  44671  hbimpgVD  45020  notnotrALTVD  45031  climxrre  45872  liminf0  45915  prprelprb  47641  prminf2  47712  nn0o1gt2ALTV  47818  nn0oALTV  47820  gbowge7  47887  nnsum3primesle9  47918  bgoldbtbndlem1  47929  usgrexmpl12ngrlic  48163  pgnbgreunbgrlem2  48241  lindslinindsimp1  48582