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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm2.24  125  jarl  126  jarli  127  pm2.18d  128  simplim  168  orel2  904  curryax  907  pm2.42  957  pm4.82  1041  pm5.71  1045  dedlem0b  1060  dedlemb  1062  cases2ALT  1064  cad0  1651  meredith  1674  tbw-bijust  1731  tbw-negdf  1732  nfntht  1826  19.38  1872  19.35  1910  sbrimvw  2128  sbn1  2144  ax13dgen2  2175  ax13dgen4  2177  nfim1  2237  sbi2  2337  dfmoeu  2562  nexmo  2568  2mo  2675  axin2  2723  r19.35  3122  r19.21v  3189  nrexrmo  3386  elab3gf  3641  elab3g  3642  moeq3  3673  dfss2  3920  rzal  4453  falseral0  4473  ralidmw  4475  ralidm  4476  opthpr  4814  opthprneg  4828  dfopif  4833  dvdemo1  5342  axprlem1  5392  axpr  5396  axprlem1OLD  5397  axprlem5OLD  5400  axprg  5406  snopeqop  5487  weniso  7361  dfwe2  7777  ordunisuc2  7844  0mnnnnn0  12564  nn0ge2m1nn  12602  xrub  13368  injresinjlem  13850  fleqceilz  13919  addmodlteq  14014  fsuppmapnn0fiub0  14061  expnngt1  14309  hashnnn0genn0  14411  hashprb  14465  hash1snb  14488  hashgt12el  14491  hashgt12el2  14492  hash2prde  14539  hashge2el2dif  14549  hashge2el2difr  14550  dvdsaddre2b  16403  lcmf  16729  prmgaplem5  17153  cshwshashlem1  17193  acsfn  17753  symgfix2  19549  0ringnnzr  20692  mndifsplit  22864  symgmatr01lem  22881  xkopt  23887  umgrislfupgrlem  29587  lfgrwlkprop  30157  frgr3vlem1  30761  frgrwopreg  30811  frgrregorufr  30813  frgrregord013  30883  9p10ne21fool  30959  satffunlem1lem1  35989  satffunlem2lem1  35991  antnestlaw1  36278  antnestlaw2  36279  jath  36312  hbimtg  36391  meran1  37038  imsym1  37045  ordcmp  37074  dfttc4lem2  37156  mh-infprim1bi  37173  bj-babygodel  37312  bj-ssbid2ALT  37401  wl-lem-nexmo  38338  nexmo1  39005  mopickr  39127  axc5c7toc7  39794  axc5c711toc7  39801  axc5c711to11  39802  ax12indi  39825  eu6w  43530  onsucf1olem  44119  dflim5  44178  ifpim23g  44343  clsk1indlem3  44891  pm10.53  45198  pm11.63  45227  axc5c4c711  45233  axc5c4c711toc5  45234  axc5c4c711toc7  45236  axc5c4c711to11  45237  3ornot23  45340  notnotrALT  45360  hbimpg  45385  hbimpgVD  45734  notnotrALTVD  45745  climxrre  46586  liminf0  46629  quantgodelALT  47711  prprelprb  48425  prminf2  48499  nn0o1gt2ALTV  48618  nn0oALTV  48620  gbowge7  48687  nnsum3primesle9  48718  bgoldbtbndlem1  48729  usgrexmpl12ngrlic  48963  pgnbgreunbgrlem2  49041  lindslinindsimp1  49395