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  899  curryax  902  pm2.42  953  pm4.82  1034  pm5.71  1038  dedlem0b  1053  dedlemb  1055  cases2ALT  1057  cad0  1628  meredith  1651  tbw-bijust  1708  tbw-negdf  1709  nfntht  1803  19.38  1849  19.35  1887  sbrimvw  2114  sbn1  2131  ax13dgen2  2162  ax13dgen4  2164  nfim1  2224  sbi2  2326  dfmoeu  2552  nexmo  2558  2mo  2665  axin2  2713  r19.35  3110  r19.21v  3177  nrexrmo  3376  elab3gf  3634  elab3g  3635  moeq3  3665  dfss2  3913  rzal  4438  falseral0  4458  ralidmw  4460  ralidm  4461  opthpr  4799  opthprneg  4813  dfopif  4818  dvdemo1  5320  axprlem1  5370  axpr  5374  axprlem1OLD  5375  axprlem5OLD  5378  axprg  5384  snopeqop  5465  weniso  7323  dfwe2  7742  ordunisuc2  7809  0mnnnnn0  12499  nn0ge2m1nn  12537  xrub  13301  injresinjlem  13782  fleqceilz  13850  addmodlteq  13945  fsuppmapnn0fiub0  13992  expnngt1  14240  hashnnn0genn0  14342  hashprb  14396  hash1snb  14418  hashgt12el  14421  hashgt12el2  14422  hash2prde  14469  hashge2el2dif  14479  hashge2el2difr  14480  dvdsaddre2b  16313  lcmf  16639  prmgaplem5  17063  cshwshashlem1  17103  acsfn  17663  symgfix2  19428  0ringnnzr  20543  mndifsplit  22665  symgmatr01lem  22682  xkopt  23684  umgrislfupgrlem  29258  lfgrwlkprop  29821  frgr3vlem1  30410  frgrwopreg  30460  frgrregorufr  30462  frgrregord013  30532  9p10ne21fool  30608  satffunlem1lem1  35690  satffunlem2lem1  35692  antnestlaw1  35979  antnestlaw2  35980  jath  36013  hbimtg  36092  meran1  36709  imsym1  36716  ordcmp  36745  dfttc4lem2  36827  mh-infprim1bi  36844  bj-babygodel  36984  bj-ssbid2ALT  37073  wl-lem-nexmo  38008  nexmo1  38686  mopickr  38808  axc5c7toc7  39475  axc5c711toc7  39482  axc5c711to11  39483  ax12indi  39506  eu6w  43196  onsucf1olem  43785  dflim5  43844  ifpim23g  44009  clsk1indlem3  44557  pm10.53  44880  pm11.63  44909  axc5c4c711  44915  axc5c4c711toc5  44916  axc5c4c711toc7  44918  axc5c4c711to11  44919  3ornot23  45023  notnotrALT  45043  hbimpg  45068  hbimpgVD  45417  notnotrALTVD  45428  climxrre  46262  liminf0  46305  quantgodelALT  47387  prprelprb  48061  prminf2  48135  nn0o1gt2ALTV  48254  nn0oALTV  48256  gbowge7  48323  nnsum3primesle9  48354  bgoldbtbndlem1  48365  usgrexmpl12ngrlic  48599  pgnbgreunbgrlem2  48677  lindslinindsimp1  49017