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 405
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 404 . 2 ((𝜑𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
31, 2mpbi 232 1 ¬ (𝜑 ∧ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  pm4.43  1018  pssirr  4075  indifdir  4258  dfnul2  4291  dfnul2OLD  4292  dfnul3  4293  noel  4294  rabnc  4339  ralnralall  4456  imadif  6431  fiint  8787  kmlem16  9583  zorn2lem4  9913  nnunb  11885  indstr  12308  bwth  22010  lgsquadlem2  25949  frgrregord013  28166  difrab2  30253  ifeqeqx  30289  ballotlemodife  31743  sgn3da  31787  poimirlem30  34909  clsk1indlem4  40379  atnaiana  43144  plcofph  43165
  Copyright terms: Public domain W3C validator