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  2206  sbi2  2308  dfmoeu  2535  nexmo  2541  2mo  2648  axin2  2697  r19.35  3094  r19.21v  3161  nrexrmo  3369  elab3gf  3639  elab3g  3640  moeq3  3670  dfss2  3919  rzal  4447  falseral0  4467  ralidmw  4469  ralidm  4470  opthpr  4807  opthprneg  4821  dfopif  4826  dvdemo1  5318  axprlem1  5368  axpr  5372  axprlem5OLD  5375  snopeqop  5454  weniso  7300  dfwe2  7719  ordunisuc2  7786  0mnnnnn0  12433  nn0ge2m1nn  12471  xrub  13227  injresinjlem  13706  fleqceilz  13774  addmodlteq  13869  fsuppmapnn0fiub0  13916  expnngt1  14164  hashnnn0genn0  14266  hashprb  14320  hash1snb  14342  hashgt12el  14345  hashgt12el2  14346  hash2prde  14393  hashge2el2dif  14403  hashge2el2difr  14404  dvdsaddre2b  16234  lcmf  16560  prmgaplem5  16983  cshwshashlem1  17023  acsfn  17582  symgfix2  19345  0ringnnzr  20458  mndifsplit  22580  symgmatr01lem  22597  xkopt  23599  umgrislfupgrlem  29195  lfgrwlkprop  29759  frgr3vlem1  30348  frgrwopreg  30398  frgrregorufr  30400  frgrregord013  30470  9p10ne21fool  30546  satffunlem1lem1  35596  satffunlem2lem1  35598  antnestlaw1  35885  antnestlaw2  35886  jath  35919  hbimtg  35998  meran1  36605  imsym1  36612  ordcmp  36641  bj-babygodel  36803  bj-ssbid2ALT  36864  wl-lem-nexmo  37768  nexmo1  38441  mopickr  38552  axc5c7toc7  39169  axc5c711toc7  39176  axc5c711to11  39177  ax12indi  39200  eu6w  42915  onsucf1olem  43508  dflim5  43567  ifpim23g  43732  clsk1indlem3  44280  pm10.53  44603  pm11.63  44632  axc5c4c711  44638  axc5c4c711toc5  44639  axc5c4c711toc7  44641  axc5c4c711to11  44642  3ornot23  44746  notnotrALT  44766  hbimpg  44791  hbimpgVD  45140  notnotrALTVD  45151  climxrre  45990  liminf0  46033  prprelprb  47759  prminf2  47830  nn0o1gt2ALTV  47936  nn0oALTV  47938  gbowge7  48005  nnsum3primesle9  48036  bgoldbtbndlem1  48047  usgrexmpl12ngrlic  48281  pgnbgreunbgrlem2  48359  lindslinindsimp1  48699