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  901  curryax  904  pm2.42  955  pm4.82  1036  pm5.71  1040  dedlem0b  1055  dedlemb  1057  cases2ALT  1059  cad0  1637  meredith  1660  tbw-bijust  1717  tbw-negdf  1718  nfntht  1812  19.38  1858  19.35  1896  sbrimvw  2123  sbn1  2140  ax13dgen2  2171  ax13dgen4  2173  nfim1  2233  sbi2  2335  dfmoeu  2561  nexmo  2567  2mo  2674  axin2  2722  r19.35  3119  r19.21v  3186  nrexrmo  3385  elab3gf  3643  elab3g  3644  moeq3  3674  dfss2  3922  rzal  4447  falseral0  4467  ralidmw  4469  ralidm  4470  opthpr  4808  opthprneg  4822  dfopif  4827  dvdemo1  5329  axprlem1  5379  axpr  5383  axprlem1OLD  5384  axprlem5OLD  5387  axprg  5393  snopeqop  5474  weniso  7334  dfwe2  7753  ordunisuc2  7820  0mnnnnn0  12510  nn0ge2m1nn  12548  xrub  13312  injresinjlem  13793  fleqceilz  13861  addmodlteq  13956  fsuppmapnn0fiub0  14003  expnngt1  14251  hashnnn0genn0  14353  hashprb  14407  hash1snb  14429  hashgt12el  14432  hashgt12el2  14433  hash2prde  14480  hashge2el2dif  14490  hashge2el2difr  14491  dvdsaddre2b  16324  lcmf  16650  prmgaplem5  17074  cshwshashlem1  17114  acsfn  17674  symgfix2  19439  0ringnnzr  20554  mndifsplit  22676  symgmatr01lem  22693  xkopt  23695  umgrislfupgrlem  29269  lfgrwlkprop  29832  frgr3vlem1  30421  frgrwopreg  30471  frgrregorufr  30473  frgrregord013  30543  9p10ne21fool  30619  satffunlem1lem1  35716  satffunlem2lem1  35718  antnestlaw1  36005  antnestlaw2  36006  jath  36039  hbimtg  36118  meran1  36735  imsym1  36742  ordcmp  36771  dfttc4lem2  36853  mh-infprim1bi  36870  bj-babygodel  37010  bj-ssbid2ALT  37099  wl-lem-nexmo  38034  nexmo1  38712  mopickr  38834  axc5c7toc7  39501  axc5c711toc7  39508  axc5c711to11  39509  ax12indi  39532  eu6w  43222  onsucf1olem  43811  dflim5  43870  ifpim23g  44035  clsk1indlem3  44583  pm10.53  44906  pm11.63  44935  axc5c4c711  44941  axc5c4c711toc5  44942  axc5c4c711toc7  44944  axc5c4c711to11  44945  3ornot23  45049  notnotrALT  45069  hbimpg  45094  hbimpgVD  45443  notnotrALTVD  45454  climxrre  46288  liminf0  46331  quantgodelALT  47413  prprelprb  48087  prminf2  48161  nn0o1gt2ALTV  48280  nn0oALTV  48282  gbowge7  48349  nnsum3primesle9  48380  bgoldbtbndlem1  48391  usgrexmpl12ngrlic  48625  pgnbgreunbgrlem2  48703  lindslinindsimp1  49043