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  1618  meredith  1641  tbw-bijust  1698  tbw-negdf  1699  nfntht  1793  19.38  1839  19.35  1877  sbn1  2107  ax13dgen2  2138  ax13dgen4  2140  nfim1  2199  sbi2  2302  dfmoeu  2536  nexmo  2541  2mo  2648  axin2  2697  r19.35  3108  r19.35OLD  3109  r19.21v  3180  nrexrmo  3401  elab3gf  3684  elab3g  3685  moeq3  3718  dfss2  3969  ralidmw  4508  rzal  4509  ralidm  4512  opthpr  4851  opthprneg  4865  dfopif  4870  dvdemo1  5373  axprlem1  5423  axpr  5427  axprlem5OLD  5430  snopeqop  5511  weniso  7374  dfwe2  7794  ordunisuc2  7865  0mnnnnn0  12558  nn0ge2m1nn  12596  xrub  13354  injresinjlem  13826  fleqceilz  13894  addmodlteq  13987  fsuppmapnn0fiub0  14034  expnngt1  14280  hashnnn0genn0  14382  hashprb  14436  hash1snb  14458  hashgt12el  14461  hashgt12el2  14462  hash2prde  14509  hashge2el2dif  14519  hashge2el2difr  14520  dvdsaddre2b  16344  lcmf  16670  prmgaplem5  17093  cshwshashlem1  17133  acsfn  17702  symgfix2  19434  0ringnnzr  20525  mndifsplit  22642  symgmatr01lem  22659  xkopt  23663  umgrislfupgrlem  29139  lfgrwlkprop  29705  frgr3vlem1  30292  frgrwopreg  30342  frgrregorufr  30344  frgrregord013  30414  9p10ne21fool  30490  satffunlem1lem1  35407  satffunlem2lem1  35409  jath  35725  hbimtg  35807  meran1  36412  imsym1  36419  ordcmp  36448  bj-babygodel  36604  bj-ssbid2ALT  36664  wl-lem-nexmo  37568  wl-ax11-lem2  37587  nexmo1  38249  mopickr  38364  axc5c7toc7  38914  axc5c711toc7  38921  axc5c711to11  38922  ax12indi  38945  eu6w  42686  onsucf1olem  43283  dflim5  43342  ifpim23g  43508  clsk1indlem3  44056  pm10.53  44385  pm11.63  44414  axc5c4c711  44420  axc5c4c711toc5  44421  axc5c4c711toc7  44423  axc5c4c711to11  44424  3ornot23  44529  notnotrALT  44549  hbimpg  44574  hbimpgVD  44924  notnotrALTVD  44935  climxrre  45765  liminf0  45808  prprelprb  47504  prminf2  47575  nn0o1gt2ALTV  47681  nn0oALTV  47683  gbowge7  47750  nnsum3primesle9  47781  bgoldbtbndlem1  47792  usgrexmpl12ngrlic  47998  lindslinindsimp1  48374