Theorem pm2.21 124

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 125 and its associated inference is pm2.21i 120. (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 23	. 2 ⊢ (¬ 𝜑 → ¬ 𝜑)
2	1	pm2.21d 122	1 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.24  125  jarl  126  jarli  127  pm2.18d  128  simplim  168  orel2  904  curryax  907  pm2.42  957  pm4.82  1041  pm5.71  1045  dedlem0b  1060  dedlemb  1062  cases2ALT  1064  cad0  1650  meredith  1673  tbw-bijust  1730  tbw-negdf  1731  nfntht  1825  19.38  1871  19.35  1909  sbrimvw  2127  sbn1  2143  ax13dgen2  2174  ax13dgen4  2176  nfim1  2235  sbi2  2335  dfmoeu  2560  nexmo  2566  2mo  2673  axin2  2721  r19.35  3120  r19.21v  3187  nrexrmo  3384  elab3gf  3637  elab3g  3638  moeq3  3669  dfss2  4094  rzal  4449  falseral0  4469  ralidmw  4471  ralidm  4472  opthpr  4805  opthprneg  4819  dfopif  4836  dvdemo1  5334  axprlem1  5384  axpr  5388  axprlem1OLD  5389  axprg  5394  snopeqop  5477  weniso  7365  dfwe2  7789  ordunisuc2  7856  0mnnnnn0  12642  nn0ge2m1nn  12680  xrub  13446  injresinjlem  13929  fleqceilz  13998  addmodlteq  14093  fsuppmapnn0fiub0  14140  expnngt1  14389  hashnnn0genn0  14491  hashprb  14545  hash1snb  14568  hashgt12el  14571  hashgt12el2  14572  hash2prde  14619  hashge2el2dif  14629  hashge2el2difr  14630  dvdsaddre2b  16483  lcmf  16814  prmgaplem5  17239  cshwshashlem1  17279  acsfn  17839  symgfix2  19636  0ringnnzr  20782  mndifsplit  22957  symgmatr01lem  22974  xkopt  23980  umgrislfupgrlem  29706  lfgrwlkprop  30276  frgr3vlem1  30880  frgrwopreg  30930  frgrregorufr  30932  frgrregord013  31002  9p10ne21fool  31078  rmo6  35757  satffunlem1lem1  36254  satffunlem2lem1  36256  antnestlaw1  36543  antnestlaw2  36544  jath  36583  hbimtg  36661  meran1  37292  imsym1  37299  ordcmp  37328  dfttc4lem2  37410  mh-infprim1bi  37427  bj-babygodel  37566  bj-ssbid2ALT  37655  wl-lem-nexmo  38593  nexmo1  39275  mopickr  39397  axc5c7toc7  40064  axc5c711toc7  40071  axc5c711to11  40072  ax12indi  40095  eu6w  43781  onsucf1olem  44366  dflim5  44425  ifpim23g  44590  clsk1indlem3  45137  pm10.53  45444  pm11.63  45473  axc5c4c711  45479  axc5c4c711toc5  45480  axc5c4c711toc7  45482  axc5c4c711to11  45483  3ornot23  45586  notnotrALT  45606  hbimpg  45631  hbimpgVD  45980  notnotrALTVD  45991  climxrre  46854  liminf0  46897  quantgodelALT  47979  prprelprb  48693  prminf2  48767  nn0o1gt2ALTV  48886  nn0oALTV  48888  gbowge7  48955  nnsum3primesle9  48986  bgoldbtbndlem1  48997  usgrexmpl12ngrlic  49231  pgnbgreunbgrlem2  49309  lindslinindsimp1  49663