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

Theorem pm2.21 102
Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. (Contributed by NM, 5-Aug-1993.) (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 20 . 2  |-  ( -. 
ph  ->  -.  ph )
21pm2.21d 100 1  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.24  103  pm2.18  104  notnot2  106  simplim  145  jarl  157  orel2  373  pm2.42  558  pm4.82  895  pm5.71  903  dedlem0b  920  dedlemb  922  dfnot  1341  cad0  1409  meredith  1413  tbw-bijust  1472  tbw-negdf  1473  ax12dgen2  1741  19.38  1812  nfimdOLD  1828  hbimdOLD  1835  hbimOLD  1837  a16gOLD  2049  sbi2  2120  ax46to6  2240  ax467to6  2247  ax467to7  2248  ax11indi  2272  mo  2302  mo2  2309  exmo  2325  2mo  2358  axin2  2405  nrexrmo  2917  elab3gf  3079  moeq3  3103  opthpr  3968  dfopif  3973  dvdemo1  4391  reusv6OLD  4726  dfwe2  4754  ordunisuc2  4816  weniso  6067  0neqopab  6111  bropopvvv  6418  xrub  10880  injresinjlem  11189  hashnnn0genn0  11617  hashprb  11658  hash1snb  11671  hashgt12el  11672  hashgt12el2  11673  hash2prde  11678  acsfn  13874  xkopt  17677  wlkdvspthlem  21597  usgrcyclnl2  21618  constr3trllem2  21628  hbimtg  25422  meran1  26126  imsym1  26133  ordcmp  26162  wl-jarli  26178  wl-pm5.74  26193  pm10.53  27493  pm11.63  27526  ax4567  27533  ax4567to4  27534  ax4567to6  27536  ax4567to7  27537  0mnnnnn0  28044  euhash1  28109  swrdvalodm2  28124  cshwssizelem1a  28206  cshwssizelem3  28209  frgra3vlem1  28291  2pthfrgra  28302  frgrancvvdeqlem2  28321  frgrawopreglem3  28336  frgraregorufr  28343  3ornot23  28492  notnot2ALT  28514  hbimpg  28542  hbimpgVD  28917  notnot2ALTVD  28928  a16gNEW7  29447  sbi2NEW7  29465
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator