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 111
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 136. (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 109 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  112  pm2.18  113  notnot2  116  simplim  156  jarl  168  orel2  390  pm2.42  584  pm4.82  942  pm5.71  950  dedlem0b  969  dedlemb  971  cases2  982  cad0  1528  meredith  1532  tbw-bijust  1589  tbw-negdf  1590  19.38  1720  19.35  1748  ax13dgen2  1929  sbi2  2242  mo2v  2326  exmo  2344  2mo  2400  axin2  2440  nrexrmo  2998  elab3gf  3178  moeq3  3203  opthpr  4144  dfopif  4155  dvdemo1  4635  weniso  6263  0neqopab  6353  dfwe2  6627  ordunisuc2  6690  0mnnnnn0  10926  nn0ge2m1nn  10958  xrub  11622  injresinjlem  12056  fleqceilz  12114  addmodlteq  12198  fsuppmapnn0fiub0  12243  hashnnn0genn0  12564  hashprb  12612  hash1snb  12634  hashgt12el  12636  hashgt12el2  12637  hash2prde  12672  hashge2el2dif  12678  hashge2el2difr  12679  lcmf  14685  prmgaplem5  15104  cshwshashlem1  15144  acsfn  15643  symgfix2  17135  0ringnnzr  18570  mndifsplit  19738  symgmatr01lem  19755  xkopt  20747  wlkdvspthlem  25416  usgrcyclnl2  25448  constr3trllem2  25458  clwlknclwlkdifs  25767  frgra3vlem1  25807  2pthfrgra  25818  frgrancvvdeqlem2  25838  frgrawopreglem3  25853  frgraregorufr  25860  frgraregord013  25925  hbimtg  30524  meran1  31142  imsym1  31149  ordcmp  31178  bj-babygodel  31251  bj-ssbid2ALT  31323  bj-dvdemo1  31483  wl-jarli  31912  wl-lem-nexmo  31966  wl-ax11-lem2  31980  tsim2  32437  axc5c7toc7  32548  axc5c711toc7  32555  axc5c711to11  32556  ax12indi  32579  ifpim23g  36210  pm10.53  36785  pm11.63  36815  axc5c4c711  36822  axc5c4c711toc5  36823  axc5c4c711toc7  36825  axc5c4c711to11  36826  3ornot23  36935  notnot2ALT  36956  hbimpg  36991  hbimpgVD  37364  notnot2ALTVD  37375  nn0o1gt2ALTV  38968  nn0oALTV  38970  gboge7  39009  nnsum3primesle9  39034  bgoldbtbndlem1  39045  umgrislfupgrlem  39367  lfgrwlkprop  39879  lindslinindsimp1  40758
  Copyright terms: Public domain W3C validator