MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pm2.21 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  1338  cad0  1406  meredith  1410  tbw-bijust  1469  tbw-negdf  1470  ax12dgen2  1737  19.38  1808  nfimdOLD  1824  hbimdOLD  1831  hbimOLD  1833  a16gOLD  2013  sbi2  2113  ax46to6  2214  ax467to6  2221  ax467to7  2222  ax11indi  2246  mo  2276  mo2  2283  exmo  2299  2mo  2332  nrexrmo  2885  elab3gf  3047  moeq3  3071  opthpr  3936  dfopif  3941  dvdemo1  4359  reusv6OLD  4693  dfwe2  4721  ordunisuc2  4783  weniso  6034  0neqopab  6078  bropopvvv  6385  xrub  10846  injresinjlem  11154  hashnnn0genn0  11582  hashprb  11623  hash1snb  11636  hashgt12el  11637  hashgt12el2  11638  hash2prde  11643  acsfn  13839  xkopt  17640  wlkdvspthlem  21560  usgrcyclnl2  21581  constr3trllem2  21591  hbimtg  25377  meran1  26065  imsym1  26072  ordcmp  26101  wl-jarli  26117  wl-pm5.74  26132  pm10.53  27429  pm11.63  27462  ax4567  27469  ax4567to4  27470  ax4567to6  27472  ax4567to7  27473  0mnnnnn0  27971  euhash1  27998  frgra3vlem1  28104  2pthfrgra  28115  frgrancvvdeqlem2  28134  frgrawopreglem3  28149  frgraregorufr  28156  3ornot23  28302  notnot2ALT  28324  hbimpg  28352  hbimpgVD  28725  notnot2ALTVD  28736  a16gNEW7  29250  sbi2NEW7  29268
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator