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 402
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 401 . 2 ((𝜑𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
31, 2mpbi 230 1 ¬ (𝜑 ∧ ¬ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  pm4.43  1024  pssirr  4102  dfnul4  4334  dfnul3  4336  rabnc  4390  ralnralall  4514  imadif  6649  fiint  9367  fiintOLD  9368  kmlem16  10207  zorn2lem4  10540  nnunb  12524  indstr  12959  bwth  23419  lgsquadlem2  27426  frgrregord013  30415  difrab2  32518  ifeqeqx  32556  ballotlemodife  34501  sgn3da  34545  sbn1ALT  36860  poimirlem30  37658  clsk1indlem4  44062  atnaiana  46940  plcofph  46961
  Copyright terms: Public domain W3C validator