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  1912  sbrimvw  2130  sbn1  2146  ax13dgen2  2177  ax13dgen4  2179  nfim1  2239  sbi2  2339  dfmoeu  2563  nexmo  2569  2mo  2676  axin2  2724  r19.35  3124  r19.21v  3191  nrexrmo  3388  elab3gf  3641  elab3g  3642  moeq3  3673  dfss2  4097  rzal  4453  falseral0  4473  ralidmw  4475  ralidm  4476  opthpr  4809  opthprneg  4823  dfopif  4840  dvdemo1  5340  axprlem1  5390  axpr  5394  axprlem1OLD  5395  axprg  5400  snopeqop  5483  weniso  7390  dfwe2  7815  ordunisuc2  7882  0mnnnnn0  12668  nn0ge2m1nn  12706  xrub  13472  injresinjlem  13955  fleqceilz  14024  addmodlteq  14119  fsuppmapnn0fiub0  14166  expnngt1  14415  hashnnn0genn0  14517  hashprb  14571  hash1snb  14594  hashgt12el  14597  hashgt12el2  14598  hash2prde  14645  hashge2el2dif  14655  hashge2el2difr  14656  dvdsaddre2b  16509  lcmf  16840  prmgaplem5  17265  cshwshashlem1  17305  acsfn  17865  symgfix2  19663  0ringnnzr  20809  mndifsplit  22984  symgmatr01lem  23001  xkopt  24007  umgrislfupgrlem  29733  lfgrwlkprop  30303  frgr3vlem1  30907  frgrwopreg  30957  frgrregorufr  30959  frgrregord013  31029  9p10ne21fool  31105  rmo6  35793  satffunlem1lem1  36347  satffunlem2lem1  36349  antnestlaw1  36636  antnestlaw2  36637  jath  36681  hbimtg  36759  meran1  37390  imsym1  37397  ordcmp  37426  dfttc4lem2  37508  mh-infprim1bi  37525  bj-babygodel  37664  bj-ssbid2ALT  37753  wl-lem-nexmo  38704  nexmo1  39384  mopickr  39506  axc5c7toc7  40173  axc5c711toc7  40180  axc5c711to11  40181  ax12indi  40204  eu6w  43891  onsucf1olem  44475  dflim5  44534  ifpim23g  44699  clsk1indlem3  45246  pm10.53  45553  pm11.63  45582  axc5c4c711  45588  axc5c4c711toc5  45589  axc5c4c711toc7  45591  axc5c4c711to11  45592  3ornot23  45694  notnotrALT  45714  hbimpg  45739  hbimpgVD  46088  notnotrALTVD  46099  climxrre  46975  liminf0  47018  quantgodelALT  48100  prprelprb  48814  prminf2  48888  nn0o1gt2ALTV  49007  nn0oALTV  49009  gbowge7  49076  nnsum3primesle9  49107  bgoldbtbndlem1  49118  usgrexmpl12ngrlic  49352  pgnbgreunbgrlem2  49430  lindslinindsimp1  49784