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  1802  nfimdOLDOLD  1821  ax13dgen2  2012  ax13dgen4  2014  nfim1  2065  sbi2  2392  mo2v  2476  exmo  2494  2mo  2550  axin2  2590  nrexrmo  3156  elab3gf  3344  moeq3  3370  opthpr  4359  dfopif  4374  dvdemo1  4873  weniso  6569  0neqopab  6663  dfwe2  6943  ordunisuc2  7006  0mnnnnn0  11285  nn0ge2m1nn  11320  xrub  12101  injresinjlem  12544  fleqceilz  12609  addmodlteq  12701  fsuppmapnn0fiub0  12749  hashnnn0genn0  13087  hashprb  13141  hash1snb  13163  hashgt12el  13166  hashgt12el2  13167  hash2prde  13206  hashge2el2dif  13216  hashge2el2difr  13217  dvdsaddre2b  14972  lcmf  15289  prmgaplem5  15702  cshwshashlem1  15745  acsfn  16260  symgfix2  17776  0ringnnzr  19209  mndifsplit  20382  symgmatr01lem  20399  xkopt  21398  umgrislfupgrlem  25946  lfgrwlkprop  26487  clwwlknclwwlkdifs  26774  frgr3vlem1  27035  frgrncvvdeqlem2  27062  frgrwopreglem3  27075  frgrregorufr  27082  frgrregord013  27141  hbimtg  31466  meran1  32105  imsym1  32112  ordcmp  32141  bj-curry  32237  bj-babygodel  32283  bj-ssbid2ALT  32341  bj-dvdemo1  32498  wl-jarli  32960  wl-lem-nexmo  33020  wl-ax11-lem2  33034  tsim2  33609  axc5c7toc7  33717  axc5c711toc7  33724  axc5c711to11  33725  ax12indi  33748  ifpim23g  37360  clsk1indlem3  37862  pm10.53  38086  pm11.63  38116  axc5c4c711  38123  axc5c4c711toc5  38124  axc5c4c711toc7  38126  axc5c4c711to11  38127  3ornot23  38236  notnotrALT  38256  hbimpg  38291  hbimpgVD  38662  notnotrALTVD  38673  prminf2  40829  nn0o1gt2ALTV  40934  nn0oALTV  40936  gboge7  40976  nnsum3primesle9  41001  bgoldbtbndlem1  41012  lindslinindsimp1  41564
  Copyright terms: Public domain W3C validator