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 403
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 402 . 2 ((𝜑𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
31, 2mpbi 231 1 ¬ (𝜑 ∧ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  pm4.43  1016  pssirr  4076  indifdir  4259  dfnul2  4292  dfnul2OLD  4293  dfnul3  4294  noel  4295  rabnc  4340  ralnralall  4456  imadif  6432  fiint  8784  kmlem16  9580  zorn2lem4  9910  nnunb  11882  indstr  12305  bwth  21948  lgsquadlem2  25885  frgrregord013  28102  difrab2  30189  ifeqeqx  30225  ballotlemodife  31655  sgn3da  31699  poimirlem30  34804  clsk1indlem4  40274  atnaiana  43040  plcofph  43061
  Copyright terms: Public domain W3C validator