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 921
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 438 . 2 ((𝜑𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
31, 2mpbi 218 1 ¬ (𝜑 ∧ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  pm4.43  963  pssirr  3668  indifdir  3841  dfnul2  3875  dfnul3  3876  rabnc  3915  axnulOLD  4711  imadif  5873  fiint  8099  kmlem16  8847  zorn2lem4  9181  nnunb  11135  indstr  11588  zeneo  14847  bwth  20965  lgsquadlem2  24823  frgrareg  26410  frgraregord013  26411  ifeqeqx  28551  ballotlemodife  29692  sgn3da  29736  poimirlem30  32405  clsk1indlem4  37158  atnaiana  39536  plcofph  39557  ralnralall  40105  av-frgraregord013  41544
  Copyright terms: Public domain W3C validator