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

Theorem pm2.21 111
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 134. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 14-Sep-2012.)
Assertion
Ref Expression
pm2.21  |-  ( -. 
ph  ->  ( ph  ->  ps ) )

Proof of Theorem pm2.21
StepHypRef Expression
1 id 23 . 2  |-  ( -. 
ph  ->  -.  ph )
21pm2.21d 109 1  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
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  112  pm2.18  113  notnot2  115  simplim  154  jarl  166  orel2  384  pm2.42  576  pm4.82  936  pm5.71  944  dedlem0b  961  dedlemb  963  cases2  980  dfnotOLD  1457  cad0  1515  meredith  1519  tbw-bijust  1577  tbw-negdf  1578  19.38  1707  19.35  1732  ax13dgen2  1884  sbi2  2187  mo2v  2272  mo2vOLD  2273  exmo  2291  2mo  2347  2moOLD  2348  axin2  2389  nrexrmo  3048  elab3gf  3223  moeq3  3248  opthpr  4175  dfopif  4181  dvdemo1  4652  weniso  6256  0neqopab  6345  dfwe2  6618  ordunisuc2  6681  0mnnnnn0  10902  nn0ge2m1nn  10934  xrub  11597  injresinjlem  12023  fleqceilz  12080  fsuppmapnn0fiub0  12204  hashnnn0genn0  12525  hashprb  12573  hash1snb  12590  hashgt12el  12592  hashgt12el2  12593  hash2prde  12628  hashge2el2dif  12633  hashge2el2difr  12634  lcmf  14593  prmgaplem5  15012  cshwshashlem1  15053  acsfn  15552  symgfix2  17044  0ringnnzr  18480  mndifsplit  19647  symgmatr01lem  19664  xkopt  20656  wlkdvspthlem  25322  usgrcyclnl2  25354  constr3trllem2  25364  clwlknclwlkdifs  25673  frgra3vlem1  25713  2pthfrgra  25724  frgrancvvdeqlem2  25744  frgrawopreglem3  25759  frgraregorufr  25766  frgraregord013  25831  hbimtg  30447  meran1  31063  imsym1  31070  ordcmp  31099  bj-babygodel  31177  bj-dvdemo1  31374  wl-jarli  31755  wl-lem-nexmo  31809  wl-ax11-lem2  31829  tsim2  32286  axc5c7toc7  32402  axc5c711toc7  32409  axc5c711to11  32410  ax12indi  32433  ifpim23g  36058  pm10.53  36572  pm11.63  36602  axc5c4c711  36609  axc5c4c711toc5  36610  axc5c4c711toc7  36612  axc5c4c711to11  36613  3ornot23  36722  notnot2ALT  36743  hbimpg  36778  hbimpgVD  37161  notnot2ALTVD  37172  nn0o1gt2ALTV  38534  nn0oALTV  38536  gboge7  38575  nnsum3primesle9  38600  bgoldbtbndlem1  38611  lindslinindsimp1  39523
  Copyright terms: Public domain W3C validator