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 406
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 405 . 2 ((𝜑𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
31, 2mpbi 233 1 ¬ (𝜑 ∧ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  pm4.43  1022  pssirr  3991  indifdirOLD  4176  dfnul4  4213  dfnul3  4215  dfnul2OLD  4216  dfnul3OLD  4217  noelOLD  4220  rabnc  4276  ralnralall  4405  imadif  6423  fiint  8869  kmlem16  9665  zorn2lem4  9999  nnunb  11972  indstr  12398  bwth  22161  lgsquadlem2  26117  frgrregord013  28332  difrab2  30419  ifeqeqx  30459  ballotlemodife  32034  sgn3da  32078  sbn1ALT  34673  poimirlem30  35430  clsk1indlem4  41200  atnaiana  43957  plcofph  43978
  Copyright terms: Public domain W3C validator