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  941  pm4.82  1022  pm5.71  1026  dedlem0b  1043  dedlemb  1045  cases2ALT  1047  cad0  1619  cad0OLD  1620  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  nfntht  1795  19.38  1841  19.35  1880  sbn1  2105  ax13dgen2  2134  ax13dgen4  2136  nfim1  2192  sbi2  2298  dfmoeu  2529  nexmo  2534  2mo  2643  axin2  2691  r19.35  3107  r19.35OLD  3108  r19.21v  3172  nrexrmo  3372  elab3gf  3639  elab3g  3640  moeq3  3673  ralidmw  4470  rzal  4471  ralidm  4474  opthpr  4814  opthprneg  4827  dfopif  4832  dvdemo1  5333  axprlem1  5383  axprlem5  5387  snopeqop  5468  0nelopabOLD  5530  weniso  7304  dfwe2  7713  ordunisuc2  7785  0mnnnnn0  12454  nn0ge2m1nn  12491  xrub  13241  injresinjlem  13702  fleqceilz  13769  addmodlteq  13861  fsuppmapnn0fiub0  13908  expnngt1  14154  hashnnn0genn0  14253  hashprb  14307  hash1snb  14329  hashgt12el  14332  hashgt12el2  14333  hash2prde  14381  hashge2el2dif  14391  hashge2el2difr  14392  dvdsaddre2b  16200  lcmf  16520  prmgaplem5  16938  cshwshashlem1  16979  acsfn  17553  symgfix2  19212  0ringnnzr  20212  mndifsplit  22022  symgmatr01lem  22039  xkopt  23043  umgrislfupgrlem  28136  lfgrwlkprop  28698  frgr3vlem1  29280  frgrwopreg  29330  frgrregorufr  29332  frgrregord013  29402  9p10ne21fool  29478  satffunlem1lem1  34083  satffunlem2lem1  34085  jath  34383  hbimtg  34467  meran1  34959  imsym1  34966  ordcmp  34995  bj-babygodel  35144  bj-ssbid2ALT  35203  wl-lem-nexmo  36095  wl-ax11-lem2  36111  nexmo1  36778  mopickr  36897  axc5c7toc7  37448  axc5c711toc7  37455  axc5c711to11  37456  ax12indi  37479  onsucf1olem  41663  dflim5  41722  ifpim23g  41889  clsk1indlem3  42437  pm10.53  42768  pm11.63  42797  axc5c4c711  42803  axc5c4c711toc5  42804  axc5c4c711toc7  42806  axc5c4c711to11  42807  3ornot23  42913  notnotrALT  42933  hbimpg  42958  hbimpgVD  43308  notnotrALTVD  43319  climxrre  44111  liminf0  44154  prprelprb  45829  prminf2  45900  nn0o1gt2ALTV  46006  nn0oALTV  46008  gbowge7  46075  nnsum3primesle9  46106  bgoldbtbndlem1  46117  lindslinindsimp1  46658