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

Theorem pm2.21 112
Description: From a wff and its negation, anything is true. Theorem *2.21 of [WhiteheadRussell] p. 104. Also called the Duns Scotus law. Its associated inference is pm2.21i 135. (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 110 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  113  pm2.18  114  notnot2  116  simplim  155  jarl  167  orel2  385  pm2.42  578  pm4.82  939  pm5.71  947  dedlem0b  964  dedlemb  966  cases2  983  cad0  1520  meredith  1524  tbw-bijust  1581  tbw-negdf  1582  19.38  1712  19.35  1740  ax13dgen2  1912  sbi2  2222  mo2v  2306  exmo  2324  2mo  2380  axin2  2420  nrexrmo  3012  elab3gf  3190  moeq3  3215  opthpr  4153  dfopif  4163  dvdemo1  4635  weniso  6245  0neqopab  6334  dfwe2  6608  ordunisuc2  6671  0mnnnnn0  10902  nn0ge2m1nn  10934  xrub  11597  injresinjlem  12024  fleqceilz  12081  fsuppmapnn0fiub0  12205  hashnnn0genn0  12526  hashprb  12574  hash1snb  12593  hashgt12el  12595  hashgt12el2  12596  hash2prde  12631  hashge2el2dif  12637  hashge2el2difr  12638  lcmf  14606  prmgaplem5  15025  cshwshashlem1  15066  acsfn  15565  symgfix2  17057  0ringnnzr  18493  mndifsplit  19661  symgmatr01lem  19678  xkopt  20670  wlkdvspthlem  25337  usgrcyclnl2  25369  constr3trllem2  25379  clwlknclwlkdifs  25688  frgra3vlem1  25728  2pthfrgra  25739  frgrancvvdeqlem2  25759  frgrawopreglem3  25774  frgraregorufr  25781  frgraregord013  25846  hbimtg  30453  meran1  31071  imsym1  31078  ordcmp  31107  bj-babygodel  31187  bj-ssbid2ALT  31259  bj-dvdemo1  31417  wl-jarli  31842  wl-lem-nexmo  31896  wl-ax11-lem2  31916  tsim2  32373  axc5c7toc7  32484  axc5c711toc7  32491  axc5c711to11  32492  ax12indi  32515  ifpim23g  36139  pm10.53  36715  pm11.63  36745  axc5c4c711  36752  axc5c4c711toc5  36753  axc5c4c711toc7  36755  axc5c4c711to11  36756  3ornot23  36865  notnot2ALT  36886  hbimpg  36921  hbimpgVD  37301  notnot2ALTVD  37312  nn0o1gt2ALTV  38823  nn0oALTV  38825  gboge7  38864  nnsum3primesle9  38889  bgoldbtbndlem1  38900  lindslinindsimp1  40303
  Copyright terms: Public domain W3C validator