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

Theorem pm3.24 882
Description: Law of noncontradiction. Theorem *3.24 of [WhiteheadRussell] p. 111 (who call it the "law of contradiction"). (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Assertion
Ref Expression
pm3.24

Proof of Theorem pm3.24
StepHypRef Expression
1 id 22 . 2
2 iman 424 . 2
31, 2mpbi 208 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  ->wi 4  /\wa 369
This theorem is referenced by:  pm4.43  927  stoic1a  1605  nonconneOLD  2666  pssirr  3603  indifdir  3753  dfnul2  3786  dfnul3  3787  rabnc  3809  axnul  4580  imadif  5668  fiint  7817  kmlem16  8566  zorn2lem4  8900  nnunb  10816  indstr  11179  bwth  19910  lgsquadlem2  23630  frgrareg  25117  frgraregord013  25118  ifeqeqx  27419  ballotlemodife  28436  sgn3da  28480  ralnralall  32294
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
  Copyright terms: Public domain W3C validator