Theorem pm2.21 123

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 124 and its associated inference is pm2.21i 119. (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 121	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  124  jarl  125  jarli  126  pm2.18d  127  simplim  167  orel2  891  curryax  894  pm2.42  945  pm4.82  1026  pm5.71  1030  dedlem0b  1045  dedlemb  1047  cases2ALT  1049  cad0  1620  meredith  1643  tbw-bijust  1700  tbw-negdf  1701  nfntht  1795  19.38  1841  19.35  1879  sbn1  2113  ax13dgen2  2144  ax13dgen4  2146  nfim1  2207  sbi2  2309  dfmoeu  2535  nexmo  2541  2mo  2648  axin2  2697  r19.35  3095  r19.21v  3162  nrexrmo  3361  elab3gf  3627  elab3g  3628  moeq3  3658  dfss2  3907  rzal  4434  falseral0  4454  ralidmw  4456  ralidm  4457  opthpr  4794  opthprneg  4808  dfopif  4813  dvdemo1  5315  axprlem1  5365  axpr  5369  axprlem1OLD  5370  axprlem5OLD  5373  axprg  5379  snopeqop  5460  weniso  7309  dfwe2  7728  ordunisuc2  7795  0mnnnnn0  12469  nn0ge2m1nn  12507  xrub  13264  injresinjlem  13745  fleqceilz  13813  addmodlteq  13908  fsuppmapnn0fiub0  13955  expnngt1  14203  hashnnn0genn0  14305  hashprb  14359  hash1snb  14381  hashgt12el  14384  hashgt12el2  14385  hash2prde  14432  hashge2el2dif  14442  hashge2el2difr  14443  dvdsaddre2b  16276  lcmf  16602  prmgaplem5  17026  cshwshashlem1  17066  acsfn  17625  symgfix2  19391  0ringnnzr  20502  mndifsplit  22601  symgmatr01lem  22618  xkopt  23620  umgrislfupgrlem  29191  lfgrwlkprop  29754  frgr3vlem1  30343  frgrwopreg  30393  frgrregorufr  30395  frgrregord013  30465  9p10ne21fool  30541  satffunlem1lem1  35584  satffunlem2lem1  35586  antnestlaw1  35873  antnestlaw2  35874  jath  35907  hbimtg  35986  meran1  36593  imsym1  36600  ordcmp  36629  dfttc4lem2  36711  mh-infprim1bi  36728  bj-babygodel  36868  bj-ssbid2ALT  36957  wl-lem-nexmo  37892  nexmo1  38570  mopickr  38692  axc5c7toc7  39359  axc5c711toc7  39366  axc5c711to11  39367  ax12indi  39390  eu6w  43109  onsucf1olem  43698  dflim5  43757  ifpim23g  43922  clsk1indlem3  44470  pm10.53  44793  pm11.63  44822  axc5c4c711  44828  axc5c4c711toc5  44829  axc5c4c711toc7  44831  axc5c4c711to11  44832  3ornot23  44936  notnotrALT  44956  hbimpg  44981  hbimpgVD  45330  notnotrALTVD  45341  climxrre  46178  liminf0  46221  quantgodelALT  47303  prprelprb  47977  prminf2  48051  nn0o1gt2ALTV  48170  nn0oALTV  48172  gbowge7  48239  nnsum3primesle9  48270  bgoldbtbndlem1  48281  usgrexmpl12ngrlic  48515  pgnbgreunbgrlem2  48593  lindslinindsimp1  48933