Theorem pm2.21 121

Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. 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  pm2.18  123  jarl  126  jarli  127  simplim  164  orel2  869  pm2.42  920  pm4.82  1005  pm5.71  1013  dedlem0b  1029  dedlemb  1031  cases2ALT  1033  cad0  1704  meredith  1714  tbw-bijust  1771  tbw-negdf  1772  19.38  1914  19.35  1957  nfimdOLDOLD  1975  ax13dgen2  2170  ax13dgen4  2172  nfim1  2221  sbi2  2540  mo2v  2625  exmo  2643  2mo  2700  axin2  2740  nrexrmo  3312  elab3gf  3508  moeq3  3536  opthpr  4516  preqsnd  4524  opthprneg  4532  dfopif  4537  dvdemo1  5031  snopeqop  5099  weniso  6748  0neqopab  6846  dfwe2  7129  ordunisuc2  7192  0mnnnnn0  11528  nn0ge2m1nn  11563  xrub  12348  injresinjlem  12797  fleqceilz  12862  addmodlteq  12954  fsuppmapnn0fiub0  13001  hashnnn0genn0  13336  hashprb  13388  hash1snb  13410  hashgt12el  13413  hashgt12el2  13414  hash2prde  13455  hashge2el2dif  13465  hashge2el2difr  13466  dvdsaddre2b  15239  lcmf  15555  prmgaplem5  15967  cshwshashlem1  16010  acsfn  16528  symgfix2  18044  0ringnnzr  19485  mndifsplit  20661  symgmatr01lem  20679  xkopt  21680  umgrislfupgrlem  26239  lfgrwlkprop  26820  clwwlknclwwlkdifsOLD  27130  frgr3vlem1  27456  frgrwopreg  27506  frgrregorufr  27508  frgrregord013  27595  jath  31948  hbimtg  32049  meran1  32748  imsym1  32755  ordcmp  32784  bj-curry  32880  bj-babygodel  32926  bj-ssbid2ALT  32984  bj-dvdemo1  33139  wl-lem-nexmo  33684  wl-ax11-lem2  33698  tsim2  34271  nexmo  34356  axc5c7toc7  34722  axc5c711toc7  34729  axc5c711to11  34730  ax12indi  34753  ifpim23g  38367  clsk1indlem3  38868  pm10.53  39092  pm11.63  39122  axc5c4c711  39129  axc5c4c711toc5  39130  axc5c4c711toc7  39132  axc5c4c711to11  39133  3ornot23  39241  notnotrALT  39261  hbimpg  39296  hbimpgVD  39663  notnotrALTVD  39674  climxrre  40501  liminf0  40544  prminf2  42029  nn0o1gt2ALTV  42134  nn0oALTV  42136  gbowge7  42180  nnsum3primesle9  42211  bgoldbtbndlem1  42222  lindslinindsimp1  42775