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  1651  meredith  1674  tbw-bijust  1731  tbw-negdf  1732  nfntht  1826  19.38  1872  19.35  1910  sbrimvw  2128  sbn1  2145  ax13dgen2  2176  ax13dgen4  2178  nfim1  2238  sbi2  2340  dfmoeu  2566  nexmo  2572  2mo  2679  axin2  2727  r19.35  3126  r19.21v  3193  nrexrmo  3391  elab3gf  3646  elab3g  3647  moeq3  3678  dfss2  3926  rzal  4460  falseral0  4480  ralidmw  4482  ralidm  4483  opthpr  4821  opthprneg  4835  dfopif  4840  dvdemo1  5349  axprlem1  5399  axpr  5403  axprlem1OLD  5404  axprlem5OLD  5407  axprg  5413  snopeqop  5494  weniso  7365  dfwe2  7782  ordunisuc2  7849  0mnnnnn0  12554  nn0ge2m1nn  12592  xrub  13356  injresinjlem  13838  fleqceilz  13907  addmodlteq  14002  fsuppmapnn0fiub0  14049  expnngt1  14297  hashnnn0genn0  14399  hashprb  14453  hash1snb  14476  hashgt12el  14479  hashgt12el2  14480  hash2prde  14527  hashge2el2dif  14537  hashge2el2difr  14538  dvdsaddre2b  16390  lcmf  16716  prmgaplem5  17140  cshwshashlem1  17180  acsfn  17740  symgfix2  19517  0ringnnzr  20660  mndifsplit  22830  symgmatr01lem  22847  xkopt  23849  umgrislfupgrlem  29509  lfgrwlkprop  30072  frgr3vlem1  30661  frgrwopreg  30711  frgrregorufr  30713  frgrregord013  30783  9p10ne21fool  30859  satffunlem1lem1  35915  satffunlem2lem1  35917  antnestlaw1  36204  antnestlaw2  36205  jath  36238  hbimtg  36317  meran1  36963  imsym1  36970  ordcmp  36999  dfttc4lem2  37081  mh-infprim1bi  37098  bj-babygodel  37237  bj-ssbid2ALT  37326  wl-lem-nexmo  38263  nexmo1  38939  mopickr  39061  axc5c7toc7  39728  axc5c711toc7  39735  axc5c711to11  39736  ax12indi  39759  eu6w  43449  onsucf1olem  44038  dflim5  44097  ifpim23g  44262  clsk1indlem3  44810  pm10.53  45117  pm11.63  45146  axc5c4c711  45152  axc5c4c711toc5  45153  axc5c4c711toc7  45155  axc5c4c711to11  45156  3ornot23  45259  notnotrALT  45279  hbimpg  45304  hbimpgVD  45653  notnotrALTVD  45664  climxrre  46505  liminf0  46548  quantgodelALT  47630  prprelprb  48307  prminf2  48381  nn0o1gt2ALTV  48500  nn0oALTV  48502  gbowge7  48569  nnsum3primesle9  48600  bgoldbtbndlem1  48611  usgrexmpl12ngrlic  48845  pgnbgreunbgrlem2  48923  lindslinindsimp1  49278