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

Theorem pm2.21 100
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 19 . 2  |-  ( -. 
ph  ->  -.  ph )
21pm2.21d 98 1  |-  ( -. 
ph  ->  ( ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4
This theorem is referenced by:  pm2.24  101  pm2.18  102  notnot2  104  simplim  143  jarl  155  orel2  372  pm2.42  557  pm4.82  894  pm5.71  902  dedlem0b  919  dedlemb  921  dfnot  1322  cad0  1390  meredith  1394  tbw-bijust  1453  tbw-negdf  1454  ax12dgen2  1712  hbimd  1733  hbim  1737  nfimd  1773  a16g  1898  sbi2  2017  ax46to6  2116  ax467to6  2123  ax467to7  2124  ax11indi  2148  mo  2178  mo2  2185  exmo  2201  2mo  2234  nrexrmo  2770  elab3gf  2932  moeq3  2955  opthpr  3806  dfopif  3809  dvdemo1  4226  reusv6OLD  4561  dfwe2  4589  ordunisuc2  4651  weniso  5868  xrub  10646  acsfn  13577  xkopt  17365  hbimtg  24234  meran1  24922  imsym1  24929  ordcmp  24958  wl-jarli  24974  wl-pm5.74  24990  lineval5a  26191  lppotoslem  26246  pm10.53  27664  pm11.63  27697  ax4567  27704  ax4567to4  27705  ax4567to6  27707  ax4567to7  27708  fnchoice  27803  conimpf  27989  0neqopab  28192  injresinjlem  28214  hashgt12el  28218  hashgt12el2  28219  trlonprop  28341  wlkdvspthlem  28365  usgrcyclnl2  28387  constr3trllem2  28397  frgra3vlem1  28424  3ornot23  28569  notnot2ALT  28591  hbimpg  28619  hbimpgVD  28996  notnot2ALTVD  29007  notnot2ALT2  29019  a16gNEW7  29521  sbi2NEW7  29539  ax9lem9  29770  ax9lem10  29771
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
  Copyright terms: Public domain W3C validator