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 962
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 220 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 197  df-an 385
This theorem is referenced by:  annotanannotOLD  978  pm4.43  1006  pssirr  3849  indifdir  4026  dfnul2  4060  dfnul3  4061  rabnc  4105  ralnralall  4224  imadif  6134  fiint  8404  kmlem16  9199  zorn2lem4  9533  nnunb  11500  indstr  11969  bwth  21435  lgsquadlem2  25326  frgrregord013  27584  difrab2  29667  ifeqeqx  29689  ballotlemodife  30889  sgn3da  30933  poimirlem30  33770  clsk1indlem4  38862  atnaiana  41614  plcofph  41635
  Copyright terms: Public domain W3C validator