Theorem pm2.21 119

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 115. (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 117	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  120  pm2.18  121  notnotr  124  simplim  162  jarl  174  orel2  397  pm2.42  596  pm4.82  965  pm5.71  973  dedlem0b  992  dedlemb  994  cases2  1005  cad0  1547  meredith  1557  tbw-bijust  1614  tbw-negdf  1615  19.38  1757  19.35  1794  nfimd  1812  ax13dgen2  2002  ax13dgen4  2004  nfim1  2055  sbi2  2381  mo2v  2465  exmo  2483  2mo  2539  axin2  2579  nrexrmo  3140  elab3gf  3325  moeq3  3350  opthpr  4324  dfopif  4337  dvdemo1  4829  weniso  6504  0neqopab  6596  dfwe2  6873  ordunisuc2  6936  0mnnnnn0  11202  nn0ge2m1nn  11237  xrub  12014  injresinjlem  12450  fleqceilz  12515  addmodlteq  12607  fsuppmapnn0fiub0  12655  hashnnn0genn0  12993  hashprb  13046  hash1snb  13068  hashgt12el  13070  hashgt12el2  13071  hash2prde  13109  hashge2el2dif  13117  hashge2el2difr  13118  dvdsaddre2b  14867  lcmf  15184  prmgaplem5  15597  cshwshashlem1  15640  acsfn  16143  symgfix2  17659  0ringnnzr  19090  mndifsplit  20261  symgmatr01lem  20278  xkopt  21268  umgrislfupgrlem  25788  wlkdvspthlem  26137  usgrcyclnl2  26169  constr3trllem2  26179  clwlknclwlkdifs  26487  frgra3vlem1  26527  2pthfrgra  26538  frgrancvvdeqlem2  26558  frgrawopreglem3  26573  frgraregorufr  26580  frgraregord013  26645  hbimtg  30956  meran1  31580  imsym1  31587  ordcmp  31616  bj-curry  31712  bj-babygodel  31761  bj-ssbid2ALT  31835  bj-dvdemo1  31990  wl-jarli  32468  wl-lem-nexmo  32528  wl-ax11-lem2  32542  tsim2  33108  axc5c7toc7  33216  axc5c711toc7  33223  axc5c711to11  33224  ax12indi  33247  ifpim23g  36859  clsk1indlem3  37361  pm10.53  37587  pm11.63  37617  axc5c4c711  37624  axc5c4c711toc5  37625  axc5c4c711toc7  37627  axc5c4c711to11  37628  3ornot23  37736  notnotrALT  37756  hbimpg  37791  hbimpgVD  38162  notnotrALTVD  38173  prminf2  40038  nn0o1gt2ALTV  40143  nn0oALTV  40145  gboge7  40185  nnsum3primesle9  40210  bgoldbtbndlem1  40221  lfgrwlkprop  40896  clwwlknclwwlkdifs  41181  frgr3vlem1  41443  frgrncvvdeqlem2  41470  frgrwopreglem3  41483  frgrregorufr  41490  av-frgraregord013  41549  lindslinindsimp1  42040