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 ⊢ (¬ 𝜑 → (𝜑 → 𝜓))

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  125  jarl  126  jarli  127  pm2.18d  128  simplim  168  orel2  903  curryax  906  pm2.42  957  pm4.82  1041  pm5.71  1045  dedlem0b  1060  dedlemb  1062  cases2ALT  1064  cad0  1648  meredith  1671  tbw-bijust  1728  tbw-negdf  1729  nfntht  1823  19.38  1869  19.35  1907  sbrimvw  2125  sbn1  2142  ax13dgen2  2173  ax13dgen4  2175  nfim1  2235  sbi2  2337  dfmoeu  2563  nexmo  2569  2mo  2676  axin2  2724  r19.35  3123  r19.21v  3190  nrexrmo  3388  elab3gf  3644  elab3g  3645  moeq3  3676  dfss2  3924  rzal  4456  falseral0  4476  ralidmw  4478  ralidm  4479  opthpr  4817  opthprneg  4831  dfopif  4836  dvdemo1  5346  axprlem1  5396  axpr  5400  axprlem1OLD  5401  axprlem5OLD  5404  axprg  5410  snopeqop  5491  weniso  7354  dfwe2  7774  ordunisuc2  7841  0mnnnnn0  12537  nn0ge2m1nn  12575  xrub  13339  injresinjlem  13821  fleqceilz  13889  addmodlteq  13984  fsuppmapnn0fiub0  14031  expnngt1  14279  hashnnn0genn0  14381  hashprb  14435  hash1snb  14458  hashgt12el  14461  hashgt12el2  14462  hash2prde  14509  hashge2el2dif  14519  hashge2el2difr  14520  dvdsaddre2b  16366  lcmf  16692  prmgaplem5  17116  cshwshashlem1  17156  acsfn  17716  symgfix2  19487  0ringnnzr  20610  mndifsplit  22774  symgmatr01lem  22791  xkopt  23793  umgrislfupgrlem  29453  lfgrwlkprop  30016  frgr3vlem1  30605  frgrwopreg  30655  frgrregorufr  30657  frgrregord013  30727  9p10ne21fool  30803  satffunlem1lem1  35875  satffunlem2lem1  35877  antnestlaw1  36164  antnestlaw2  36165  jath  36198  hbimtg  36277  meran1  36903  imsym1  36910  ordcmp  36939  dfttc4lem2  37021  mh-infprim1bi  37038  bj-babygodel  37177  bj-ssbid2ALT  37266  wl-lem-nexmo  38203  nexmo1  38879  mopickr  39001  axc5c7toc7  39668  axc5c711toc7  39675  axc5c711to11  39676  ax12indi  39699  eu6w  43391  onsucf1olem  43980  dflim5  44039  ifpim23g  44204  clsk1indlem3  44752  pm10.53  45059  pm11.63  45088  axc5c4c711  45094  axc5c4c711toc5  45095  axc5c4c711toc7  45097  axc5c4c711to11  45098  3ornot23  45201  notnotrALT  45221  hbimpg  45246  hbimpgVD  45595  notnotrALTVD  45606  climxrre  46447  liminf0  46490  quantgodelALT  47572  prprelprb  48249  prminf2  48323  nn0o1gt2ALTV  48442  nn0oALTV  48444  gbowge7  48511  nnsum3primesle9  48542  bgoldbtbndlem1  48553  usgrexmpl12ngrlic  48787  pgnbgreunbgrlem2  48865  lindslinindsimp1  49220