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

Theorem pm3.24 392
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 391 . 2 ((𝜑𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
31, 2mpbi 222 1 ¬ (𝜑 ∧ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 385
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 199  df-an 386
This theorem is referenced by:  annotanannotOLD  1035  pm4.43  1047  pssirr  3905  indifdir  4085  dfnul2  4118  dfnul3  4119  rabnc  4161  ralnralall  4272  imadif  6185  fiint  8480  kmlem16  9276  zorn2lem4  9610  nnunb  11575  indstr  12000  bwth  21541  lgsquadlem2  25457  frgrregord013  27779  difrab2  29856  ifeqeqx  29878  ballotlemodife  31075  sgn3da  31119  poimirlem30  33927  clsk1indlem4  39119  atnaiana  41831  plcofph  41852
  Copyright terms: Public domain W3C validator