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  2536  nexmo  2542  2mo  2649  axin2  2698  r19.35  3096  r19.21v  3163  nrexrmo  3362  elab3gf  3628  elab3g  3629  moeq3  3659  dfss2  3908  rzal  4435  falseral0  4455  ralidmw  4457  ralidm  4458  opthpr  4795  opthprneg  4809  dfopif  4814  dvdemo1  5310  axprlem1  5360  axpr  5364  axprlem1OLD  5365  axprlem5OLD  5368  axprg  5374  snopeqop  5454  weniso  7302  dfwe2  7721  ordunisuc2  7788  0mnnnnn0  12460  nn0ge2m1nn  12498  xrub  13255  injresinjlem  13736  fleqceilz  13804  addmodlteq  13899  fsuppmapnn0fiub0  13946  expnngt1  14194  hashnnn0genn0  14296  hashprb  14350  hash1snb  14372  hashgt12el  14375  hashgt12el2  14376  hash2prde  14423  hashge2el2dif  14433  hashge2el2difr  14434  dvdsaddre2b  16267  lcmf  16593  prmgaplem5  17017  cshwshashlem1  17057  acsfn  17616  symgfix2  19382  0ringnnzr  20493  mndifsplit  22611  symgmatr01lem  22628  xkopt  23630  umgrislfupgrlem  29205  lfgrwlkprop  29769  frgr3vlem1  30358  frgrwopreg  30408  frgrregorufr  30410  frgrregord013  30480  9p10ne21fool  30556  satffunlem1lem1  35600  satffunlem2lem1  35602  antnestlaw1  35889  antnestlaw2  35890  jath  35923  hbimtg  36002  meran1  36609  imsym1  36616  ordcmp  36645  dfttc4lem2  36727  mh-infprim1bi  36744  bj-babygodel  36884  bj-ssbid2ALT  36973  wl-lem-nexmo  37906  nexmo1  38584  mopickr  38706  axc5c7toc7  39373  axc5c711toc7  39380  axc5c711to11  39381  ax12indi  39404  eu6w  43123  onsucf1olem  43716  dflim5  43775  ifpim23g  43940  clsk1indlem3  44488  pm10.53  44811  pm11.63  44840  axc5c4c711  44846  axc5c4c711toc5  44847  axc5c4c711toc7  44849  axc5c4c711to11  44850  3ornot23  44954  notnotrALT  44974  hbimpg  44999  hbimpgVD  45348  notnotrALTVD  45359  climxrre  46196  liminf0  46239  prprelprb  47989  prminf2  48063  nn0o1gt2ALTV  48182  nn0oALTV  48184  gbowge7  48251  nnsum3primesle9  48282  bgoldbtbndlem1  48293  usgrexmpl12ngrlic  48527  pgnbgreunbgrlem2  48605  lindslinindsimp1  48945