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

Theorem pm2.21 108
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, 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 22 . 2  |-  ( -. 
ph  ->  -.  ph )
21pm2.21d 106 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  109  pm2.18  110  notnot2  112  simplim  151  jarl  163  orel2  383  pm2.42  574  pm4.82  928  pm5.71  936  dedlem0b  953  dedlemb  955  cases2  971  ifpfal  1389  dfnotOLD  1415  cad0  1467  meredith  1472  tbw-bijust  1531  tbw-negdf  1532  19.38  1663  19.35  1688  ax13dgen2  1835  sbi2  2135  axc5c7toc7  2244  axc5c711toc7  2251  axc5c711to11  2252  ax12indi  2275  mo2v  2290  mo2vOLD  2291  mo2vOLDOLD  2292  exmo  2310  mo2OLD  2335  2mo  2373  2moOLD  2374  axin2  2424  nrexrmo  3077  elab3gf  3251  moeq3  3276  opthpr  4210  dfopif  4216  reusv6OLD  4667  dvdemo1  4691  weniso  6251  0neqopab  6340  dfwe2  6616  ordunisuc2  6678  0mnnnnn0  10849  nn0ge2m1nn  10882  xrub  11528  injresinjlem  11927  fleqceilz  11983  fsuppmapnn0fiub0  12101  hashnnn0genn0  12418  hashprb  12465  hash1snb  12482  hashgt12el  12484  hashgt12el2  12485  hash2prde  12519  hashge2el2dif  12524  cshwshashlem1  14591  acsfn  15075  symgfix2  16567  0ringnnzr  18043  mndifsplit  19264  symgmatr01lem  19281  xkopt  20281  wlkdvspthlem  24735  usgrcyclnl2  24767  constr3trllem2  24777  clwlknclwlkdifs  25086  frgra3vlem1  25126  2pthfrgra  25137  frgrancvvdeqlem2  25157  frgrawopreglem3  25172  frgraregorufr  25179  frgraregord013  25244  hbimtg  29413  meran1  30038  imsym1  30045  ordcmp  30074  wl-jarli  30132  wl-lem-nexmo  30178  wl-ax11-lem2  30188  tsim2  30700  pm10.53  31433  pm11.63  31463  axc5c4c711  31470  axc5c4c711toc5  31471  axc5c4c711toc7  31473  axc5c4c711to11  31474  lindslinindsimp1  33160  3ornot23  33379  notnot2ALT  33400  hbimpg  33428  hbimpgVD  33805  notnot2ALTVD  33816  bj-babygodel  34292  bj-dvdemo1  34489
  Copyright terms: Public domain W3C validator