Theorem pm2.21 121

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 122 and its associated inference is pm2.21i 117. (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 119	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  122  jarl  123  jarli  124  pm2.18  125  simplim  165  orel2  877  curryax  880  pm2.42  929  pm4.82  1009  pm5.71  1013  dedlem0b  1028  dedlemb  1030  cases2ALT  1032  cad0  1675  meredith  1685  tbw-bijust  1742  tbw-negdf  1743  nfntht  1837  19.38  1882  19.35  1924  ax13dgen2  2132  ax13dgen4  2134  nfim1  2182  sbi2v  2279  sbi2  2469  nexmo  2552  nexmoOLD  2553  dfmo  2615  exmoOLD  2619  2mo  2678  axin2  2741  nrexrmo  3359  elab3gf  3564  moeq3  3595  opthpr  4612  preqsnd  4620  opthprneg  4628  dfopif  4633  dvdemo1  5085  snopeqop  5202  weniso  6876  0neqopab  6975  dfwe2  7259  ordunisuc2  7322  0mnnnnn0  11676  nn0ge2m1nn  11711  xrub  12454  injresinjlem  12907  fleqceilz  12972  addmodlteq  13064  fsuppmapnn0fiub0  13111  expnngt1  13347  hashnnn0genn0  13448  hashprb  13499  hash1snb  13521  hashgt12el  13524  hashgt12el2  13525  hash2prde  13566  hashge2el2dif  13576  hashge2el2difr  13577  dvdsaddre2b  15436  lcmf  15752  prmgaplem5  16163  cshwshashlem1  16201  acsfn  16705  symgfix2  18219  0ringnnzr  19666  mndifsplit  20847  symgmatr01lem  20865  xkopt  21867  umgrislfupgrlem  26470  lfgrwlkprop  27038  frgr3vlem1  27681  frgrwopreg  27731  frgrregorufr  27733  frgrregord013  27827  jath  32206  hbimtg  32300  meran1  32993  imsym1  33000  ordcmp  33029  bj-babygodel  33167  bj-ssbid2ALT  33236  bj-dvdemo1  33378  wl-lem-nexmo  33943  wl-ax11-lem2  33957  nexmo1  34646  axc5c7toc7  35067  axc5c711toc7  35074  axc5c711to11  35075  ax12indi  35098  ifpim23g  38798  clsk1indlem3  39297  pm10.53  39521  pm11.63  39551  axc5c4c711  39557  axc5c4c711toc5  39558  axc5c4c711toc7  39560  axc5c4c711to11  39561  3ornot23  39669  notnotrALT  39689  hbimpg  39714  hbimpgVD  40073  notnotrALTVD  40084  climxrre  40890  liminf0  40933  prprelprb  42456  prminf2  42521  nn0o1gt2ALTV  42630  nn0oALTV  42632  gbowge7  42676  nnsum3primesle9  42707  bgoldbtbndlem1  42718  lindslinindsimp1  43261