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  10882  injresinjlem  11191  hashnnn0genn0  11619  hashprb  11660  hash1snb  11673  hashgt12el  11674  hashgt12el2  11675  hash2prde  11680  acsfn  13876  xkopt  17679  wlkdvspthlem  21599  usgrcyclnl2  21620  constr3trllem2  21630  hbimtg  25426  meran1  26153  imsym1  26160  ordcmp  26189  wl-jarli  26205  wl-pm5.74  26220  pm10.53  27529  pm11.63  27562  ax4567  27569  ax4567to4  27570  ax4567to6  27572  ax4567to7  27573  0mnnnnn0  28080  euhash1  28145  swrdvalodm2  28160  cshwssizelem1a  28242  cshwssizelem3  28245  frgra3vlem1  28327  2pthfrgra  28338  frgrancvvdeqlem2  28357  frgrawopreglem3  28372  frgraregorufr  28379  3ornot23  28528  notnot2ALT  28550  hbimpg  28578  hbimpgVD  28953  notnot2ALTVD  28964  a16gNEW7  29483  sbi2NEW7  29501
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator