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  890  curryax  893  pm2.42  944  pm4.82  1025  pm5.71  1029  dedlem0b  1044  dedlemb  1046  cases2ALT  1048  cad0  1619  meredith  1642  tbw-bijust  1699  tbw-negdf  1700  nfntht  1794  19.38  1840  19.35  1878  sbn1  2110  ax13dgen2  2141  ax13dgen4  2143  nfim1  2202  sbi2  2304  dfmoeu  2531  nexmo  2536  2mo  2643  axin2  2692  r19.35  3090  r19.21v  3157  nrexrmo  3365  elab3gf  3640  elab3g  3641  moeq3  3671  dfss2  3920  ralidmw  4458  rzal  4459  ralidm  4462  opthpr  4803  opthprneg  4817  dfopif  4822  dvdemo1  5311  axprlem1  5361  axpr  5365  axprlem5OLD  5368  snopeqop  5446  weniso  7288  dfwe2  7707  ordunisuc2  7774  0mnnnnn0  12410  nn0ge2m1nn  12448  xrub  13208  injresinjlem  13687  fleqceilz  13755  addmodlteq  13850  fsuppmapnn0fiub0  13897  expnngt1  14145  hashnnn0genn0  14247  hashprb  14301  hash1snb  14323  hashgt12el  14326  hashgt12el2  14327  hash2prde  14374  hashge2el2dif  14384  hashge2el2difr  14385  dvdsaddre2b  16215  lcmf  16541  prmgaplem5  16964  cshwshashlem1  17004  acsfn  17562  symgfix2  19326  0ringnnzr  20438  mndifsplit  22549  symgmatr01lem  22566  xkopt  23568  umgrislfupgrlem  29098  lfgrwlkprop  29662  frgr3vlem1  30248  frgrwopreg  30298  frgrregorufr  30300  frgrregord013  30370  9p10ne21fool  30446  satffunlem1lem1  35434  satffunlem2lem1  35436  antnestlaw1  35723  antnestlaw2  35724  jath  35757  hbimtg  35839  meran1  36444  imsym1  36451  ordcmp  36480  bj-babygodel  36636  bj-ssbid2ALT  36696  wl-lem-nexmo  37600  wl-ax11-lem2  37619  nexmo1  38281  mopickr  38390  axc5c7toc7  38951  axc5c711toc7  38958  axc5c711to11  38959  ax12indi  38982  eu6w  42708  onsucf1olem  43302  dflim5  43361  ifpim23g  43527  clsk1indlem3  44075  pm10.53  44398  pm11.63  44427  axc5c4c711  44433  axc5c4c711toc5  44434  axc5c4c711toc7  44436  axc5c4c711to11  44437  3ornot23  44541  notnotrALT  44561  hbimpg  44586  hbimpgVD  44935  notnotrALTVD  44946  climxrre  45787  liminf0  45830  prprelprb  47547  prminf2  47618  nn0o1gt2ALTV  47724  nn0oALTV  47726  gbowge7  47793  nnsum3primesle9  47824  bgoldbtbndlem1  47835  usgrexmpl12ngrlic  48069  pgnbgreunbgrlem2  48147  lindslinindsimp1  48488