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

Step	Hyp	Ref	Expression
1		id 22	. 2 ⊢ (𝜑 → 𝜑)
2		iman 401	. 2 ⊢ ((𝜑 → 𝜑) ↔ ¬ (𝜑 ∧ ¬ 𝜑))
3	1, 2	mpbi 230	1 ⊢ ¬ (𝜑 ∧ ¬ 𝜑)

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  4083  dfnul4  4315  dfnul3  4317  rabnc  4371  ralnralall  4495  imadif  6625  fiint  9343  fiintOLD  9344  kmlem16  10185  zorn2lem4  10518  nnunb  12502  indstr  12937  bwth  23353  lgsquadlem2  27349  frgrregord013  30381  difrab2  32484  ifeqeqx  32528  sgn3da  32818  ballotlemodife  34535  sbn1ALT  36881  poimirlem30  37679  clsk1indlem4  44035  atnaiana  46919  plcofph  46940