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 229 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 206  df-an 397
This theorem is referenced by:  pm4.43  1020  pssirr  4035  indifdirOLD  4219  dfnul4  4258  dfnul3  4260  dfnul2OLD  4261  dfnul3OLD  4262  noelOLD  4265  rabnc  4321  ralnralall  4449  imadif  6518  fiint  9091  kmlem16  9921  zorn2lem4  10255  nnunb  12229  indstr  12656  bwth  22561  lgsquadlem2  26529  frgrregord013  28759  difrab2  30845  ifeqeqx  30885  ballotlemodife  32464  sgn3da  32508  sbn1ALT  35042  poimirlem30  35807  clsk1indlem4  41654  atnaiana  44418  plcofph  44439
  Copyright terms: Public domain W3C validator