MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21 Structured version   Visualization version   GIF version

Theorem pm2.21 120
Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. Its associated inference is pm2.21i 116. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 14-Sep-2012.)
Assertion
Ref Expression
pm2.21 𝜑 → (𝜑𝜓))

Proof of Theorem pm2.21
StepHypRef Expression
1 id 22 . 2 𝜑 → ¬ 𝜑)
21pm2.21d 118 1 𝜑 → (𝜑𝜓))
Colors of variables: wff setvar class
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  121  pm2.18  122  notnotr  125  simplim  163  jarl  175  orel2  398  pm2.42  597  pm4.82  968  pm5.71  976  cases2  992  dedlem0b  1000  dedlemb  1002  cad0  1553  meredith  1563  tbw-bijust  1620  tbw-negdf  1621  19.38  1763  19.35  1805  nfimdOLDOLD  1826  ax13dgen2  2017  ax13dgen4  2019  nfim1  2070  sbi2  2397  mo2v  2481  exmo  2499  2mo  2555  axin2  2595  nrexrmo  3157  elab3gf  3344  moeq3  3370  opthpr  4357  dfopif  4372  dvdemo1  4868  weniso  6559  0neqopab  6652  dfwe2  6929  ordunisuc2  6992  0mnnnnn0  11270  nn0ge2m1nn  11305  xrub  12082  injresinjlem  12525  fleqceilz  12590  addmodlteq  12682  fsuppmapnn0fiub0  12730  hashnnn0genn0  13068  hashprb  13122  hash1snb  13144  hashgt12el  13147  hashgt12el2  13148  hash2prde  13187  hashge2el2dif  13195  hashge2el2difr  13196  dvdsaddre2b  14948  lcmf  15265  prmgaplem5  15678  cshwshashlem1  15721  acsfn  16236  symgfix2  17752  0ringnnzr  19183  mndifsplit  20356  symgmatr01lem  20373  xkopt  21363  umgrislfupgrlem  25907  lfgrwlkprop  26447  clwwlknclwwlkdifs  26734  frgr3vlem1  26995  frgrncvvdeqlem2  27022  frgrwopreglem3  27035  frgrregorufr  27042  frgrregord013  27101  hbimtg  31401  meran1  32025  imsym1  32032  ordcmp  32061  bj-curry  32157  bj-babygodel  32203  bj-ssbid2ALT  32261  bj-dvdemo1  32418  wl-jarli  32897  wl-lem-nexmo  32957  wl-ax11-lem2  32971  tsim2  33537  axc5c7toc7  33645  axc5c711toc7  33652  axc5c711to11  33653  ax12indi  33676  ifpim23g  37288  clsk1indlem3  37790  pm10.53  38014  pm11.63  38044  axc5c4c711  38051  axc5c4c711toc5  38052  axc5c4c711toc7  38054  axc5c4c711to11  38055  3ornot23  38164  notnotrALT  38184  hbimpg  38219  hbimpgVD  38590  notnotrALTVD  38601  prminf2  40768  nn0o1gt2ALTV  40873  nn0oALTV  40875  gboge7  40915  nnsum3primesle9  40940  bgoldbtbndlem1  40951  lindslinindsimp1  41489
  Copyright terms: Public domain W3C validator