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  1025  pssirr  4044  dfnul4  4276  dfnul3  4278  rabnc  4332  ralnralall  4454  imadif  6574  fiint  9228  kmlem16  10077  zorn2lem4  10410  nnunb  12398  indstr  12830  bwth  23353  lgsquadlem2  27332  frgrregord013  30454  difrab2  32556  ifeqeqx  32601  sgn3da  32898  ballotlemodife  34648  sbn1ALT  37163  poimirlem30  37962  clsk1indlem4  44474  atnaiana  47357  plcofph  47378