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  2144  ax13dgen2  2175  ax13dgen4  2177  nfim1  2236  sbi2  2336  dfmoeu  2561  nexmo  2567  2mo  2674  axin2  2722  r19.35  3121  r19.21v  3188  nrexrmo  3385  elab3gf  3638  elab3g  3639  moeq3  3670  dfss2  3917  rzal  4450  falseral0  4470  ralidmw  4472  ralidm  4473  opthpr  4811  opthprneg  4825  dfopif  4830  dvdemo1  5335  axprlem1  5385  axpr  5389  axprlem1OLD  5390  axprg  5395  snopeqop  5478  weniso  7356  dfwe2  7777  ordunisuc2  7844  0mnnnnn0  12619  nn0ge2m1nn  12657  xrub  13423  injresinjlem  13905  fleqceilz  13974  addmodlteq  14069  fsuppmapnn0fiub0  14116  expnngt1  14365  hashnnn0genn0  14467  hashprb  14521  hash1snb  14544  hashgt12el  14547  hashgt12el2  14548  hash2prde  14595  hashge2el2dif  14605  hashge2el2difr  14606  dvdsaddre2b  16457  lcmf  16788  prmgaplem5  17213  cshwshashlem1  17253  acsfn  17813  symgfix2  19610  0ringnnzr  20756  mndifsplit  22931  symgmatr01lem  22948  xkopt  23954  umgrislfupgrlem  29682  lfgrwlkprop  30252  frgr3vlem1  30856  frgrwopreg  30906  frgrregorufr  30908  frgrregord013  30978  9p10ne21fool  31054  satffunlem1lem1  36136  satffunlem2lem1  36138  antnestlaw1  36425  antnestlaw2  36426  jath  36459  hbimtg  36538  meran1  37169  imsym1  37176  ordcmp  37205  dfttc4lem2  37287  mh-infprim1bi  37304  bj-babygodel  37443  bj-ssbid2ALT  37532  wl-lem-nexmo  38467  nexmo1  39149  mopickr  39271  axc5c7toc7  39938  axc5c711toc7  39945  axc5c711to11  39946  ax12indi  39969  eu6w  43641  onsucf1olem  44230  dflim5  44289  ifpim23g  44454  clsk1indlem3  45002  pm10.53  45309  pm11.63  45338  axc5c4c711  45344  axc5c4c711toc5  45345  axc5c4c711toc7  45347  axc5c4c711to11  45348  3ornot23  45451  notnotrALT  45471  hbimpg  45496  hbimpgVD  45845  notnotrALTVD  45856  climxrre  46704  liminf0  46747  quantgodelALT  47829  prprelprb  48543  prminf2  48617  nn0o1gt2ALTV  48736  nn0oALTV  48738  gbowge7  48805  nnsum3primesle9  48836  bgoldbtbndlem1  48847  usgrexmpl12ngrlic  49081  pgnbgreunbgrlem2  49159  lindslinindsimp1  49513