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

Theorem pm3.24 922
 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 439 . 2 ((𝜑𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
31, 2mpbi 219 1 ¬ (𝜑 ∧ ¬ 𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  pm4.43  964  pssirr  3669  indifdir  3842  dfnul2  3876  dfnul3  3877  rabnc  3916  imadif  5887  fiint  8122  kmlem16  8870  zorn2lem4  9204  nnunb  11165  indstr  11632  zeneo  14901  bwth  21023  lgsquadlem2  24906  frgrareg  26644  frgraregord013  26645  ifeqeqx  28745  ballotlemodife  29886  sgn3da  29930  poimirlem30  32609  clsk1indlem4  37362  atnaiana  39739  plcofph  39760  ralnralall  40307  av-frgraregord013  41549
 Copyright terms: Public domain W3C validator